DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
17 stars 2 forks source link

Removes elements from the SDF #4

Closed VincentCheval closed 7 years ago

VincentCheval commented 7 years ago

We may need to add a function that removes elements from the SDF that are consequence and not used in the recipes before going through a new input or output. Since this verification would cost some computing time, we should test first on examples if that case happens a lot or not.