Automatic Verification of Security Protocols in the Symbolic Model: The Verifier Proverif

被引：87
作者：
Blanchet, Bruno [1 ]
机构：
[1] INRIA Paris-Rocquencourt, France
来源：
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | 2014年 / 8604卷
关键词：
Logic programming - Network security - Calculations;
D O I：
10.1007/978-3-319-10082-1_3
中图分类号：
学科分类号：
摘要：
After giving general context on the verification of security protocols, we focus on the automatic symbolic protocol verifier ProVerif. This verifier can prove secrecy, authentication, and observational equivalence properties of security protocols, for an unbounded number of sessions of the protocol. It supports a wide range of cryptographic primitives defined by rewrite rules or by equations. The tool takes as input a description of the protocol to verify in a process calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol into an abstract representation of the protocol by Horn clauses, and determines whether the desired security properties hold by resolution on these clauses. © Springer International Publishing Switzerland 2014.
引用
收藏
页码：54 / 87
页数：33
相关论文
共 73 条
[1]  
Abadi M., Blanchet B., Secrecy types for asymmetric communication, Theoretical Computer Science, 298, 3, pp. 387-415, (2003)
[2]  
Abadi M., Blanchet B., Analyzing security protocols with secrecy types and logic programs, Journal of the ACM, 52, 1, pp. 102-146, (2005)
[3]  
Abadi M., Blanchet B., Computer-assisted verification of a protocol for certified email, Science of Computer Programming, 58, 1-2, pp. 3-27, (2005)
[4]  
Abadi M., Blanchet B., Fournet C., Just Fast Keying in the pi calculus, ACM TISSEC, 10, 3, pp. 1-59, (2007)
[5]  
Abadi M., Fournet C., Mobile values, new names, and secure communication, pp. 104-115, (2001)
[6]  
Abadi M., Glew N., Horne B., Pinkas B., Certified email with a light on-line trusted third party: Design and implementation, 11Th Internationalworldwide Web Conference, pp. 387-395, (2002)
[7]  
Abadi M., Needham R., Prudent engineering practice for cryptographic protocols, IEEE Transactions on Software Engineering, 22, 1, pp. 6-15, (1996)
[8]  
Aiello W., Bellovin S.M., Blaze M., Canetti R., Ioannidis J., Keromytis K., Reingold O., Just Fast Keying: Key agreement in a hostile Internet, ACM TISSEC, 7, 2, pp. 242-273, (2004)
[9]  
Aizatulin M., Gordon A.D., Jurjens J., Extracting and verifying cryptographic models from C protocol code by symbolic execution, CCS 2011, pp. 331-340, (2011)
[10]  
Allamigeon X., Blanchet B., Reconstruction of attacks against cryptographic protocols, CSFW 2005, pp. 140-154, (2005)
12345678