Verification of security protocols with lists: From length one to unbounded length
Pages 781 - 816
Abstract
We present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the automatic verifier ProVerif: we show that if a protocol is proven secure by our technique with lists of length one, then it is secure for lists of unbounded length. Interestingly, this theorem relies on approximations made by our verification technique: in general, secrecy for lists of length one does not imply secrecy for lists of unbounded length. Our result can be used in particular to prove secrecy properties for group protocols with an unbounded number of participants and for some XML protocols web services with ProVerif.
References
[1]
M. Abadi and B. Blanchet, Analyzing security protocols with secrecy types and logic programs, Journal of the ACM 52(1) (2005), 102-146.
[2]
N. Asokan and P. Ginzboorg, Key agreement in ad hoc networks, Computer Communications 23(17) (2000), 1627-1637.
[3]
L. Bachmair and H. Ganzinger, Resolution theorem proving, in: Handbook of Automated Reasoning, Vol. 1, Chapter 2, North-Holland, 2001, pp. 19-100.
[4]
B. Blanchet, Using Horn clauses for analyzing security protocols, in: Formal Models and Techniques for Analyzing Security Protocols, V. Cortier and S. Kremer, eds, Cryptology and Information Security Series, Vol. 5, IOS Press, Amsterdam, 2011, pp. 86-111.
[5]
J. Bryans and S. Schneider, CSP, PVS and recursive authentication protocol, in: DIMACS Workshop on Formal Verification of Security Protocols, 1997.
[6]
N. Chridi, M. Turuani and M. Rusinowitch, Constraints-based verification of parameterized cryptographic protocols, Research Report RR-6712, INRIA, 2008.
[7]
N. Chridi, M. Turuani and M. Rusinowitch, Decidable analysis for a class of cryptographic group protocols with unbounded lists, in: CSF'09, IEEE, Los Alamitos, 2009, pp. 277-289.
[8]
D. Dolev and A.C. Yao, On the security of public key protocols, IEEE Transactions on Information Theory 29(12) (1983), 198-208.
[9]
D. Eastlake and J. Reagle, XML encryption syntax and processing, W3C Candidate Recommendation, 2002, available at: http://www.w3.org/TR/2002/CR-xmlenc-core-20020802/.
[10]
J. Goubault-Larrecq, Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve?, in: JFLA'04, INRIA, 2004, pp. 1-20.
[11]
S. Kremer, A. Mercier and R. Treinen, Proving group protocols secure against eavesdroppers, in: IJCAR'08, LNAI, Vol. 5195, Springer, Heidelberg, 2008, pp. 116-131.
[12]
R. Küsters and T. Truderung, On the automatic analysis of recursive security protocols with XOR, in: STACS'07, W. Thomas and P. Weil, eds, LNCS, Vol. 4393, Springer, Heidelberg, 2007, pp. 646-657.
[13]
R. Küsters and T. Truderung, Using Pro Verif to analyze protocols with Diffie-Hellman exponentiation, in: CSF'09, IEEE, Los Alamitos, 2009, pp. 157-171.
[14]
C. Meadows, Extending formal cryptographic protocol analysis techniques for group protocols and low-level cryptographic primitives, in: WITS'00, 2000.
[15]
C. Meadows and P. Narendran, A unification algorithm for the group Diffie-Hellman protocol, in: WITS'02, 2002.
[16]
C. Meadows, P. Syverson and I. Cervesato, Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer, Journal of Computer Security 12(6) (2004), 893-931.
[17]
L.C. Paulson, Mechanized proofs for a recursive authentication protocol, in: CSFW'97, IEEE, Los Alamitos, 1997, pp. 84-95.
[18]
O. Pereira and J.-J. Quisquater, Some attacks upon authenticated group key agreement protocols, Journal of Computer Security 11(4) (2003), 555-580.
[19]
O. Pereira and J.-J. Quisquater, Generic insecurity of cliques-type authenticated group key agreement protocols, in: CSFW'04, IEEE, Los Alamitos, 2004, pp. 16-19.
[20]
G. Steel and A. Bundy, Attacking group protocols by refuting incorrect inductive conjectures, Journal of Automated Reasoning 36(1,2) (2006), 149-176.
[21]
M. Steiner, G. Tsudik and M. Waidner, CLIQUES: A new approach to group key agreement, in: ICDCS'98, IEEE, Los Alamitos, 1998, pp. 380-387.
[22]
T. Truderung, Selecting theories and recursive protocols, in: CONCUR'05, M. Abadi and L. de Alfaro, eds, Springer, Heidelberg, 2005, pp. 217-232.
- Verification of security protocols with lists: From length one to unbounded length
Recommendations
Verification of security protocols with lists: from length one to unbounded length
POST'12: Proceedings of the First international conference on Principles of Security and TrustWe present a novel, simple technique for proving secrecy properties for security protocols that manipulate lists of unbounded length, for an unbounded number of sessions. More specifically, our technique relies on the Horn clause approach used in the ...
Formal Verification of Security Protocols: ProVerif and Extensions
Artificial Intelligence and SecurityAbstractSecure protocols are built on cryptographic algorithms, which provide a variety of secure services to realize secure communications in a network environment. To improve the quality of security protocols and ensure their reliability, sufficient ...
Automatic Verification for Secrecy of Cryptographic Protocols in First-Order Logic
In this article, we present a new formal approach for specification and automatic verification of cryptographic protocols. First, we use the first-order theory to formalize cryptographic protocols and intruders. Assuming that messages transmitted by ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
November 2013
231 pages
Publisher
IOS Press
Netherlands
Publication History
Published: 01 November 2013
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 14 Feb 2025