Syntax support for the automatic prover ProVerif
ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. Its main features are:
ProVerif can prove the following properties:
Official webpage of ProVerif: https://prosecco.gforge.inria.fr/personal/bblanche/proverif/
Good catch. Let us know what about this package looks wrong to you, and we'll investigate right away.