TY - GEN
T1 - Reconstruction of attacks against cryptographic protocols
AU - Allamigeon, Xavier
AU - Blanchet, Bruno
PY - 2005/12/6
Y1 - 2005/12/6
N2 - 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 200g 200 protocol [21].
AB - 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 200g 200 protocol [21].
UR - https://www.scopus.com/pages/publications/28144458017
U2 - 10.1109/CSFW.2005.25
DO - 10.1109/CSFW.2005.25
M3 - Conference contribution
AN - SCOPUS:28144458017
SN - 0769523404
T3 - Proceedings of the Computer Security Foundations Workshop
SP - 140
EP - 154
BT - Proceedings of the 18th IEEE Computer Security Foundations Workshop
T2 - 18th IEEE Computer Security Foundations Workshop
Y2 - 20 June 2005 through 22 June 2005
ER -