Proverif specification execution fails if typed Pi calculus isn't used
Summary
The execution of proverif returns an error if the "Generate typed Pi calculus" isn't checked.
Steps to reproduce
- Open any security model
- Click on Synthax analysis
- Click on Security Analysis (proverif)
- Uncheck Generate typed Pi calculus
- Execute the verification
What is the current bug behavior?
The result of the verification is 'Synthax error.: File "../proverif/pvspec", line 4, characters 1-3'
What is the expected correct behavior?
The same result as if the checkbox was checked should be output.
Possible fixes
The source of the issue is that the generator outputs "set abbreviateDerivation = false." instead of "param abbreviateDerivation = false." as it should be in Pi.