proverif
“ProVerif” is a powerful utility designed to examine “reachability properties,” “correspondence assertions,” and “observational equivalences.” Our protocol modelling addresses both the elemental security requirements, like “impersonation” or “replay” attack, and the most advanced ones, like “perfect forward secrecy” or “password guessing attack.”
Because we had a limited space in our published paper, the program source codes are provided here. The codes can be tested online at "http://proverif16.paris.inria.fr/".
- Categories:
We have included the code of protocol verification for ProVerif (in .pv format) and Scyther (in .spdl format) in the “Supplementary Materials” (Supplementary-Materials.pdf) of the revised manuscript. Essentially, the .pdf file of the “Supplementary Materials” includes: A. The source code for the protocol verifier Scyther (in .spdl format); and B. The source code for the protocol verifier ProVerif (in .pv format).
- Categories: