Reconstruction of attacks against cryptographic protocols

被引：22
作者：
Allamigeon, X [1 ]
Blanchet, B [1 ]
机构：
[1] Ecole Polytech, F-75230 Paris, France
来源：
18TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS | 2005年
关键词：
D O I：
10.1109/CSFW.2005.25
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We study an automatic technique for the verification of cryptographic protocols based on a Horn clause model of the protocol. This technique yields proofs valid for an unbounded number of sessions of the protocol. However, up to now, it gave no definite information when the proof failed. In this paper we present an algorithm for reconstructing an attack against the protocol when the desired security property does not hold. We have proved soundness, termination, as well as a partial completeness result for our algorithm. We have also implemented it in the automatic protocol verifier ProVerif As an extreme example, we could reconstruct an attack involving 200 parallel sessions against the f(200) g(200) protocol [21].
引用
收藏
页码：140 / 154
页数：15
相关论文
共 27 条
[11]  
Blanchet B, 2004, P IEEE S SECUR PRIV, P86
[12]  
Blanchet B, 2002, LECT NOTES COMPUT SC, V2477, P342
[13]  
Blanchet B, 2003, LECT NOTES COMPUT SC, V2620, P136
[14]   An efficient cryptographic protocol verifier based on prolog rules [J].
Blanchet, B .
14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :82-96
[15]   Capturing parallel attacks within the data independence framework [J].
Broadfoot, PJ ;
Roscoe, AW .
15TH IEEE COMPUTER SECURITY FOUNDATION WORKSHOP, PROCEEDINGS, 2002, :147-159
[16]  
BURROWS M, 1990, ACM T COMPUT SYST, V8, P18, DOI [10.1145/77648.77649, 10.1145/74851.74852]
[17]   TIMESTAMPS IN KEY DISTRIBUTION PROTOCOLS [J].
DENNING, DE ;
SACCO, GM .
COMMUNICATIONS OF THE ACM, 1981, 24 (08) :533-536
[18]  
Durgin N., 2004, Journal of Computer Security, V12, P247
[19]   Types and effects for asymmetric cryptographic protocols [J].
Gordon, AD ;
Jeffrey, A .
15TH IEEE COMPUTER SECURITY FOUNDATION WORKSHOP, PROCEEDINGS, 2002, :77-91
[20]  
GOUBAULTLARRECQ J, 2004, ACT 15 JOURN FRANC L
123