Article

Towards computationally sound symbolic analysis of key exchange protocols

Authors:

Vitaly ShmatikovAuthors Info & Claims

FMSE '05: Proceedings of the 2005 ACM workshop on Formal methods in security engineering

Pages 23 - 32

https://doi.org/10.1145/1103576.1103580

Published: 11 November 2005 Publication History

Abstract

We present a cryptographically sound formal method for proving correctness of key exchange protocols. Our main tool is a fragment of a symbolic protocol logic. We demonstrate that proofs of key agreement and key secrecy in this logic imply simulatability in Shoup's secure multi-party framework for key exchange. As part of the logic, we present cryptographically sound abstractions of CMA-secure digital signatures and a restricted form of Diffie-Hellman exponentiation, which is a technical result of independent interest. We illustrate our method by constructing a proof of security for a simple authenticated Diffie-Hellman protocol.

References

[1]

M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103--127, 2002.]]

Digital Library

[2]

M. Backes and B. Pfitzmann. Relating symbolic and cryptographic secrecy. In Proc. IEEE Symposium on Security and Privacy, pages 171--182. IEEE, 2005.]]

Digital Library

[3]

M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In Proc. 10th ACM Conference on Computer and Communications Security (CCS), pages 220--230. ACM, 2003.]]

Digital Library

[4]

M. Backes, B. Pfitzmann, and M. Waidner. A general composition theorem for secure reactive systems. In Proc. 1st Theory of Cryptography Conference (TCC), volume 3378 of LNCS, pages 336--354. Springer-Verlag, 2004.]]

[5]

D. Beaver. Secure multiparty protocols and zero-knowledge proof systems tolerating a faulty minority. J. Cryptology, 4(2):75--122, 1991.]]

Digital Library

[6]

M. Bellare, R. Canetti, and H. Krawczyk. A modular approach to the design and analysis of authentication and key exchange protocols. In Proc. 30th Annual ACM Symposium on Theory of Computing (STOC), pages 419--428. ACM, 1998.]]

Digital Library

[7]

M. Bellare and P. Rogaway. Entity authentication and key distribution. In Proc. Advances in Cryptology -- CRYPTO 1993, volume 773, pages 232--249. Springer-Verlag, 1993.]]

Digital Library

[8]

R. Bird, I. Gopal, A. Herzberg, P. Janson, S. Kutton, R. Molva, and M. Yung. Systematic design of two-party authentication protocols. In Proc. Advances in Cryptology -- CRYPTO 1991, volume 576 of LNCS, pages 44--61. Springer-Verlag, 1991.]]

Digital Library

[9]

S. Blake-Wilson, D. Johnson, and A. Menezes. Key agreement protocols and their security analysis. In Proc. 6th IMA International Conference on Cryptography and Coding, pages 30--45, 1997.]]

Digital Library

[10]

R. Canetti. Studies in secure multiparty computation and applications. PhD thesis, The Weizmann Institute of Science, 1995.]]

[11]

R. Canetti. Security and composition of multiparty cryptographic protocols. J. Cryptology, 13(1):143--202, 2000.]]

Digital Library

[12]

R. Canetti. Universally composable security: a new paradigm for cryptographic protocols. In Proc. 42nd Annual Symposium on Foundations of Computer Science (FOCS), pages 136--145. IEEE, 2001. Full version at http://eprint.iacr.org/2000/067.]]

Digital Library

[13]

R. Canetti. Universally composable signature, certification, and authentication. In Proc. 17th IEEE Computer Security Foundations Workshop (CSFW), pages 219--233. IEEE, 2004. Full version at http://eprint.iacr.org/2003/329.]]

Digital Library

[14]

R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). http://eprint.iacr.org/2004/334, 2005.]]

[15]

R. Canetti and H. Krawczyk. Analysis of key-exchange protocols and their use for building secure channels. In Proc. Advances in Cryptology - EUROCRYPT 2001, volume 2045 of LNCS, pages 453--474. Springer-Verlag, 2001.]]

Digital Library

[16]

R. Canetti and H. Krawczyk. Universally composable notions of key exchange and secure channels. In Proc. Advances in Cryptology - EUROCRYPT 2002, volume 2332 of LNCS, pages 337--351. Springer-Verlag, 2002. Full version at http://eprint.iacr.org/2002/059.]]

Digital Library

[17]

R. Canetti and T. Rabin. Universal composition with joint state. In Proc. Advances in Cryptology -- CRYPTO 2003, volume 2729 of LNCS, pages 265--281. Springer-Verlag, 2003.]]

[18]

V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In Proc. 14th European Symposium on Programming (ESOP), volume 3444 of LNCS, pages 157--171. Springer-Verlag, 2005.]]

Digital Library

[19]

A. Datta, A. Derek, J.C. Mitchell, and D. Pavlovic. A derivation system for security protocols and its logical formalization. In Proc. 16th IEEE Computer Security Foundations Workshop (CSFW), pages 109--125. IEEE, 2003.]]

[20]

A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In Proc. 32nd International Colloquium on Automata, Languages and Programming (ICALP) - to appear, 2005.]]

Digital Library

[21]

T. Dierks and C. Allen. The TLS protocol Version 1.0. Internet RFC: http://www.ietf.org/rfc/rfc2246.txt, January 1999.]]

Digital Library

[22]

W. Diffie, P. van Oorschot, and M. Wiener. Authentication and authenticated key exchange. Designs, Code, and Cryptography, 2(2):107--125, 1992.]]

Digital Library

[23]

N. Durgin, J.C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. J. Computer Security, 11(4):677--722, 2003.]]

Digital Library

[24]

O. Goldreich. Foundations of Cryptography: Volume II (Basic Applications). Cambridge University Press, 2004.]]

Digital Library

[25]

S. Goldwasser, S. Micali, and R. Rivest. A digital signature scheme secure against adaptive chosen-message attack. SIAM J. Computing, 17(2):281--308, 1988.]]

Digital Library

[26]

P. Gupta and V. Shmatikov. Towards computationally sound symbolic analysis of key exchange protocols. http://eprint.iacr.org/2005/171, 2005.]]

[27]

R. Impagliazzo and D. Zuckerman. How to recycle random bits. In Proc. 30th Annual Symposium on Foundations of Computer Science (FOCS), pages 248--253. IEEE, 1989.]]

Digital Library

[28]

C. Kaufman (ed.). Internet key exchange (IKEv2) protocol. Internet draft: http://www.ietf.org/internet-drafts/draft-ietf-ipsec-ikev2-17.txt, September 2004.]]

[29]

J. Kohl and C. Neuman. The Kerberos network authentication service (V5). Internet RFC: http://www.ietf.org/rfc/rfc1510.txt, September 1993.]]

Digital Library

[30]

P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In Proc. IEEE Symposium on Security and Privacy, pages 71--85. IEEE, 2004.]]

[31]

D. Micciancio and B. Warinschi. Completeness theorems for the Abadi-Rogaway language of encrypted expressions. J. Computer Security, 12(1):99--130, 2004.]]

Digital Library

[32]

D. Micciancio and B. Warinschi. Soundness of formal encryption in the presence of active adversaries. In Proc. 1st Theory of Cryptography Conference (TCC), volume 3378 of LNCS, pages 133--151. Springer-Verlag, 2004.]]

[33]

B. Pfitzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. In Proc. IEEE Symposium on Security and Privacy, pages 184--200. IEEE, 2001.]]

Digital Library

[34]

V. Shoup. On formal models for secure key exchange (version 4). http://shoup.net/papers/skey.pdf, November 1999.]]

[35]

F. Thayer, J. Herzog, and J. Guttman. Strand spaces: proving security protocols correct. J. Computer Security, 7(1), 1999.]]

Digital Library

Cited By

Basin DCremers C(2014)Know Your EnemyACM Transactions on Information and System Security10.1145/265899617:2(1-31)Online publication date: 17-Nov-2014
https://dl.acm.org/doi/10.1145/2658996
Aizatulin MGordon AJürjens JYu TDanezis GGligor V(2012)Computational verification of C protocol implementations by symbolic executionProceedings of the 2012 ACM conference on Computer and communications security10.1145/2382196.2382271(712-723)Online publication date: 16-Oct-2012
https://dl.acm.org/doi/10.1145/2382196.2382271
Xiao YSu K(2012)The DH exponentiation extension in a verification logic of local sessions2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE)10.1109/CSAE.2012.6272646(499-503)Online publication date: May-2012
https://doi.org/10.1109/CSAE.2012.6272646
Show More Cited By

Index Terms

Towards computationally sound symbolic analysis of key exchange protocols

Recommendations

Computationally sound analysis of protocols using bilinear pairings
7th International Workshop on Issues in the Theory of Security (WITS'07)

In this paper, we introduce a symbolic model to analyse protocols that use a bilinear pairing between two cyclic groups. This model consists in an extension of the Abadi-Rogaway logic and we prove that the logic is still computationally sound: symbolic ...
Computationally complete symbolic attacker and key exchange
CCS '13: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security

Recently, Bana and Comon-Lundh introduced the notion of computationally complete symbolic attacker to deliver unconditional computational soundness to symbolic protocol verification. First we explain the relationship between their technique and Fitting'...
Computationally sound symbolic security reduction analysis of the group key exchange protocols using bilinear pairings

The security of the group key exchange protocols has been widely studied in the cryptographic community in recent years. Current work usually applies either the computational approach or the symbolic approach for security analysis. The symbolic approach ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FMSE '05: Proceedings of the 2005 ACM workshop on Formal methods in security engineering

November 2005

90 pages

ISBN:1595932313

DOI:10.1145/1103576

General Chair:
Vijay Atluri
Rutgers University
,
Program Chairs:
Pierangela Samarati
Universita' degli Studi di Milano, Italy
,
Ralf Küsters
University of Kiel, Germany
,
John Mitchell
Stanford University

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 November 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

CCS05

Sponsor:

CCS05: 12th ACM Conference on Computer and Communications Security 2005

November 11, 2005

VA, Fairfax, USA

Upcoming Conference

CCS '24

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 14 - 18, 2024

Salt Lake City , UT , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
288
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 02 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Basin DCremers C(2014)Know Your EnemyACM Transactions on Information and System Security10.1145/265899617:2(1-31)Online publication date: 17-Nov-2014
https://dl.acm.org/doi/10.1145/2658996
Aizatulin MGordon AJürjens JYu TDanezis GGligor V(2012)Computational verification of C protocol implementations by symbolic executionProceedings of the 2012 ACM conference on Computer and communications security10.1145/2382196.2382271(712-723)Online publication date: 16-Oct-2012
https://dl.acm.org/doi/10.1145/2382196.2382271
Xiao YSu K(2012)The DH exponentiation extension in a verification logic of local sessions2012 IEEE International Conference on Computer Science and Automation Engineering (CSAE)10.1109/CSAE.2012.6272646(499-503)Online publication date: May-2012
https://doi.org/10.1109/CSAE.2012.6272646
Zhang ZZhu LLiao LWang M(2012)Computationally sound symbolic security reduction analysis of the group key exchange protocols using bilinear pairingsInformation Sciences10.1016/j.ins.2012.04.029209(93-112)Online publication date: Nov-2012
https://doi.org/10.1016/j.ins.2012.04.029
Cortier VKremer SWarinschi B(2011)A Survey of Symbolic Methods in Computational Analysis of Cryptographic SystemsJournal of Automated Reasoning10.1007/s10817-010-9187-946:3-4(225-259)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1007/s10817-010-9187-9
Roy ADatta ADerek AMitchell J(2010)Inductive trace properties for computational securityJournal of Computer Security10.5555/1891823.189182618:6(1035-1073)Online publication date: 21-Sep-2010
https://dl.acm.org/doi/10.5555/1891823.1891826
Kremer SMazaré L(2010)Computationally sound analysis of protocols using bilinear pairingsJournal of Computer Security10.5555/1891823.189182518:6(999-1033)Online publication date: 21-Sep-2010
https://dl.acm.org/doi/10.5555/1891823.1891825
Basin DCremers C(2010)Modeling and analyzing security in the presence of compromising adversariesProceedings of the 15th European conference on Research in computer security10.5555/1888881.1888908(340-356)Online publication date: 20-Sep-2010
https://dl.acm.org/doi/10.5555/1888881.1888908
Micciancio D(2010)The RSA Group is Pseudo-FreeJournal of Cryptology10.1007/s00145-009-9042-523:2(169-186)Online publication date: 1-Apr-2010
https://dl.acm.org/doi/10.1007/s00145-009-9042-5
Basin DCremers C(2010)Modeling and Analyzing Security in the Presence of Compromising AdversariesComputer Security – ESORICS 201010.1007/978-3-642-15497-3_21(340-356)Online publication date: 2010
https://doi.org/10.1007/978-3-642-15497-3_21
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents