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 条
[51]  
Godskesen J.C., Formal verification of the ARAN protocol using the applied picalculus, WITS 2006, pp. 99-113, (2006)
[52]  
Gordon A., Jeffrey A., Types and effects for asymmetric cryptographic protocols, Journal of Computer Security, 12, 3-4, pp. 435-484, (2004)
[53]  
Goubault-Larrecq J., Deciding H1 by resolution, Information Processing Letters, 95, 3, pp. 401-408, (2005)
[54]  
Goubault-Larrecq J., Parrennes F., Cryptographic protocol analysis on real C code, VMCAI 2005. LNCS, 3385, pp. 363-379, (2005)
[55]  
Heather J., Lowe G., Schneider S., How to prevent type flaw attacks on security protocols, CSFW 2000, pp. 255-268, (2000)
[56]  
Kallahalla M., Riedel E., Swaminathan R., Wang Q., Fu K., Plutus: Scalable secure file sharing on untrusted storage, FAST 2003, pp. 29-42, (2003)
[57]  
Khurana H., Hahm H.S., Certified mailing lists, ASIACCS 2006, pp. 46-58, (2006)
[58]  
Kremer S., Ryan M.D., Analysis of an electronic voting protocol in the applied pi calculus, ESOP 2005. LNCS, 3444, pp. 186-200, (2005)
[59]  
Kusters R., Truderung T., Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach, CCS 2008, pp. 129-138, (2008)
[60]  
Kusters R., Truderung T., Using ProVerif to analyze protocols with Diffie-Hellman exponentiation, CSF 2009, pp. 157-171, (2009)
12345678