Support is provided for
cryptographic primitives including:
symmetric &
asymmetric cryptography;
digital signatures; hash functions;
bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and
observational equivalence. These reasoning capabilities are particularly useful to the
computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an unbounded message space. The tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed.
Applicability of ProVerif
ProVerif has been used in the following case studies, which include the security analysis of actual network protocols:
Abadi & Blanchet[2] used correspondence assertions to verify the certified email protocol.[3]
Abadi, Blanchet & Fournet[4] analyse the Just Fast Keying[5] protocol, which was one of the candidates to replace
Internet Key Exchange (IKE) as the key exchange protocol in
IPsec, by combining manual proofs with ProVerif proofs of correspondence and equivalence.
Blanchet & Chaudhuri[6] studied the integrity of the Plutus file system[7] on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
Bhargavan et al.[8][9][10] use ProVerif to analyse cryptographic protocol implementations written in
F#; in particular the
Transport Layer Security (TLS) protocol has been studied in this manner.
Delaune, Kremer & Ryan[12][13] and Backes, Hritcu & Maffei[14] formalise and analyse privacy properties for
electronic voting using observational equivalence.
Delaune, Ryan & Smyth[15] and Backes, Maffei & Unruh[16] analyse the
anonymity properties of the trusted computing scheme
Direct Anonymous Attestation (DAA) using observational equivalence.
Alternative analysis tools include: AVISPA (for reachability and correspondence assertions), KISS (for static equivalence), YAPA (for static equivalence).
CryptoVerif for verification of security against
polynomial time adversaries in the computational model. The
Tamarin Prover is a modern alternative to ProVerif, with excellent support for Diffie-Hellman equational reasoning, and verification of observational equivalence properties.
^Abadi, Martín; Glew, Neal (2002). "Certified email with a light on-line trusted third party". Proceedings of the 11th international conference on World Wide Web. WWW '02. New York, NY, USA: ACM. pp. 387–395.
doi:
10.1145/511446.511497.
ISBN978-1581134490.
S2CID9035150.
^Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (May 2004). "Just Fast Keying: Key Agreement in a Hostile Interne". ACM Transactions on Information and System Security. 7 (2): 242–273.
doi:
10.1145/996943.996946.
ISSN1094-9224.
S2CID14442788.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08). "Verified Reference Implementations of WS-Security Protocols". Web Services and Formal Methods. Lecture Notes in Computer Science. Vol. 4184. Springer, Berlin, Heidelberg. pp. 88–106.
CiteSeerX10.1.1.61.3389.
doi:
10.1007/11841197_6.
ISBN9783540388623.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). "Verified implementations of the information card federated identity-management protocol". Proceedings of the 2008 ACM symposium on Information, computer and communications security. ASIACCS '08. New York, NY, USA: ACM. pp. 123–135.
doi:
10.1145/1368310.1368330.
ISBN9781595939791.
S2CID6821014.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (December 2008). "Verified Interoperable Implementations of Security Protocols". ACM Transactions on Programming Languages and Systems. 31 (1): 5:1–5:61.
CiteSeerX10.1.1.187.9727.
doi:
10.1145/1452044.1452049.
ISSN0164-0925.
S2CID14018835.
^Chen, Liqun; Ryan, Mark (2009-11-05). "Attack, Solution and Verification for Shared Authorisation Data in TCG TPM". Formal Aspects in Security and Trust. Lecture Notes in Computer Science. Vol. 5983. Springer, Berlin, Heidelberg. pp. 201–216.
CiteSeerX10.1.1.158.2073.
doi:
10.1007/978-3-642-12459-4_15.
ISBN9783642124587.
^Kremer, Steve; Ryan, Mark (2005-04-04). "Analysis of an Electronic Voting Protocol in the Applied Pi Calculus". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 3444. Springer, Berlin, Heidelberg. pp. 186–200.
doi:
10.1007/978-3-540-31987-0_14.
ISBN9783540254355.
^Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18). "Automatic Verification of Privacy Properties in the Applied pi Calculus". Trust Management II. IFIP – The International Federation for Information Processing. Vol. 263. Springer, Boston, MA. pp. 263–278.
doi:
10.1007/978-0-387-09428-1_17.
ISBN9780387094274.
^Backes, M.; Maffei, M.; Unruh, D. (May 2008). "Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol". 2008 IEEE Symposium on Security and Privacy (Sp 2008). pp. 202–215.
CiteSeerX10.1.1.463.489.
doi:
10.1109/SP.2008.23.
ISBN978-0-7695-3168-7.
S2CID651680.
Support is provided for
cryptographic primitives including:
symmetric &
asymmetric cryptography;
digital signatures; hash functions;
bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and
observational equivalence. These reasoning capabilities are particularly useful to the
computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an unbounded message space. The tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed.
Applicability of ProVerif
ProVerif has been used in the following case studies, which include the security analysis of actual network protocols:
Abadi & Blanchet[2] used correspondence assertions to verify the certified email protocol.[3]
Abadi, Blanchet & Fournet[4] analyse the Just Fast Keying[5] protocol, which was one of the candidates to replace
Internet Key Exchange (IKE) as the key exchange protocol in
IPsec, by combining manual proofs with ProVerif proofs of correspondence and equivalence.
Blanchet & Chaudhuri[6] studied the integrity of the Plutus file system[7] on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
Bhargavan et al.[8][9][10] use ProVerif to analyse cryptographic protocol implementations written in
F#; in particular the
Transport Layer Security (TLS) protocol has been studied in this manner.
Delaune, Kremer & Ryan[12][13] and Backes, Hritcu & Maffei[14] formalise and analyse privacy properties for
electronic voting using observational equivalence.
Delaune, Ryan & Smyth[15] and Backes, Maffei & Unruh[16] analyse the
anonymity properties of the trusted computing scheme
Direct Anonymous Attestation (DAA) using observational equivalence.
Alternative analysis tools include: AVISPA (for reachability and correspondence assertions), KISS (for static equivalence), YAPA (for static equivalence).
CryptoVerif for verification of security against
polynomial time adversaries in the computational model. The
Tamarin Prover is a modern alternative to ProVerif, with excellent support for Diffie-Hellman equational reasoning, and verification of observational equivalence properties.
^Abadi, Martín; Glew, Neal (2002). "Certified email with a light on-line trusted third party". Proceedings of the 11th international conference on World Wide Web. WWW '02. New York, NY, USA: ACM. pp. 387–395.
doi:
10.1145/511446.511497.
ISBN978-1581134490.
S2CID9035150.
^Aiello, William; Bellovin, Steven M.; Blaze, Matt; Canetti, Ran; Ioannidis, John; Keromytis, Angelos D.; Reingold, Omer (May 2004). "Just Fast Keying: Key Agreement in a Hostile Interne". ACM Transactions on Information and System Security. 7 (2): 242–273.
doi:
10.1145/996943.996946.
ISSN1094-9224.
S2CID14442788.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D. (2006-09-08). "Verified Reference Implementations of WS-Security Protocols". Web Services and Formal Methods. Lecture Notes in Computer Science. Vol. 4184. Springer, Berlin, Heidelberg. pp. 88–106.
CiteSeerX10.1.1.61.3389.
doi:
10.1007/11841197_6.
ISBN9783540388623.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Swamy, Nikhil (2008). "Verified implementations of the information card federated identity-management protocol". Proceedings of the 2008 ACM symposium on Information, computer and communications security. ASIACCS '08. New York, NY, USA: ACM. pp. 123–135.
doi:
10.1145/1368310.1368330.
ISBN9781595939791.
S2CID6821014.
^Bhargavan, Karthikeyan; Fournet, Cédric; Gordon, Andrew D.; Tse, Stephen (December 2008). "Verified Interoperable Implementations of Security Protocols". ACM Transactions on Programming Languages and Systems. 31 (1): 5:1–5:61.
CiteSeerX10.1.1.187.9727.
doi:
10.1145/1452044.1452049.
ISSN0164-0925.
S2CID14018835.
^Chen, Liqun; Ryan, Mark (2009-11-05). "Attack, Solution and Verification for Shared Authorisation Data in TCG TPM". Formal Aspects in Security and Trust. Lecture Notes in Computer Science. Vol. 5983. Springer, Berlin, Heidelberg. pp. 201–216.
CiteSeerX10.1.1.158.2073.
doi:
10.1007/978-3-642-12459-4_15.
ISBN9783642124587.
^Kremer, Steve; Ryan, Mark (2005-04-04). "Analysis of an Electronic Voting Protocol in the Applied Pi Calculus". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 3444. Springer, Berlin, Heidelberg. pp. 186–200.
doi:
10.1007/978-3-540-31987-0_14.
ISBN9783540254355.
^Delaune, Stéphanie; Ryan, Mark; Smyth, Ben (2008-06-18). "Automatic Verification of Privacy Properties in the Applied pi Calculus". Trust Management II. IFIP – The International Federation for Information Processing. Vol. 263. Springer, Boston, MA. pp. 263–278.
doi:
10.1007/978-0-387-09428-1_17.
ISBN9780387094274.
^Backes, M.; Maffei, M.; Unruh, D. (May 2008). "Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol". 2008 IEEE Symposium on Security and Privacy (Sp 2008). pp. 202–215.
CiteSeerX10.1.1.463.489.
doi:
10.1109/SP.2008.23.
ISBN978-0-7695-3168-7.
S2CID651680.