Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif
作者： Bruno Blanchet
DOI: 10.1007/978-3-319-10082-1_3
关键词:
摘要: After giving general context on the verification of security protocols, we focus automatic symbolic protocol verifier ProVerif. This can prove secrecy, authentication, and observational equivalence properties for an unbounded number sessions protocol. It supports a wide range cryptographic primitives defined by rewrite rules or equations. The tool takes as input description to verify in process calculus, extension pi calculus with cryptography. automatically translates this into abstract representation Horn clauses, determines whether desired hold resolution these clauses.
springer.com
sci-hub.st 参考文章(87)
Bruno Blanchet, Security protocol verification: symbolic and computational models principles of security and trust. ,vol. 7215, pp. 3- 29 ,(2012) , 10.1007/978-3-642-28641-4_2
Kousha Etessami, Gerard J. Holzmann, Optimizing Büchi Automata international conference on concurrency theory. pp. 153- 167 ,(2000) , 10.1007/3-540-44618-4_13
Steve Kremer, Mark Ryan, Analysis of an Electronic Voting Protocol in the Applied Pi Calculus Programming Languages and Systems. pp. 186- 200 ,(2005) , 10.1007/978-3-540-31987-0_14
Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Verified Reference Implementations of WS-Security Protocols Lecture Notes in Computer Science. ,vol. 4184, pp. 88- 106 ,(2006) , 10.1007/11841197_6
Tobias Nipkow, Orna Grumberg, Benedikt Hauptmann, Software Safety and Security: Tools for Analysis and Verification ,(2012)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Myrto Arapinis, Marie Duflot, Bounding Messages for Free in Security Protocols FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science. ,vol. 4855, pp. 376- 387 ,(2007) , 10.1007/978-3-540-77050-3_31
Leo Bachmair, Harald Ganzinger, David McAllester, Christopher Lynch, Resolution Theorem Proving Handbook of Automated Reasoning. pp. 19- 99 ,(2001) , 10.1016/B978-044450813-3/50004-7
Hubert Comon-Lundh, Véronique Cortier, New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols Rewriting Techniques and Applications. pp. 148- 164 ,(2003) , 10.1007/3-540-44881-0_12
Carolyn Whitnall, Elisabeth Oswald, A comprehensive evaluation of mutual information analysis using a fair evaluation framework international cryptology conference. ,vol. 2011, pp. 316- 334 ,(2011) , 10.1007/978-3-642-22792-9_18