Article

The faithfulness of abstract protocol analysis: message authentication

Authors:

Joshua D. Guttman,

F. Javier Thayer,

Lenore D. ZuckAuthors Info & Claims

CCS '01: Proceedings of the 8th ACM conference on Computer and Communications Security

Pages 186 - 195

https://doi.org/10.1145/501983.502009

Published: 05 November 2001 Publication History

Abstract

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable methods to determine many security properties of protocols. A separate line of work, initiated by Bellare and Rogaway, analyzes the way specific cryptographic primitives are used in protocols. It gives asymptotic bounds on the risk of failures of secrecy or authentication.In this paper we show how the Dolev-Yao model may be used for protocol analysis, while a further analysis gives a quantitative bound on the extent to which real cryptographic primitives may diverge from the idealized model. We develop this method where the cryptographic primitives are based on Carter-Wegman universal classes of hash functions. This choice allows us to give specific quantitative bounds rather than simply asymptotic bounds.

References

[1]

Martyn Abadi and Phillip Rogaway.Reconciling two views of cryptog aphy (the computational soundness of formal encryption).In IFIP International Conference on Theoreti al Computer Science (IFIP TCS2000),Lecture Notes in Compute Science. Sp inger-Verlag,2000.]]

Digital Library

[2]

Mihir Bellare.Practice-oriented provable security.In E.Okamoto,G.Davida,and M.Mambo,editors,First International Workshop on Information Se urity (ISW 97),volume 1396 of LNCS .Sp inger Verlag,1998.]]

Digital Library

[3]

Mihir Bellare,J.Killian,and Phillip Rogaway.The security of ciphe block chaining.In Yvo Desmedt, editor,Advances in Cryptology -Crypto 94,volume 839 of LNCS .Sp inger Verlag,1994.]]

Digital Library

[4]

Mihir Bellare and Phillip Rogaway.Entity authentication and key distribution.In Advances in Cryptol ogy -Crypto '93 Proceedings .Sp inger-Verlag, 1993.Full version available at http://www-cse.ucsd.edu/users/mihi /pape s/eakd.ps.]]

Digital Library

[5]

Michael Burrows,Mart~n Abadi,and Roger Needham. A logic of authentication.Proceedings of the Royal Society,Series A,426(1871):233 -271,December 1989. Also appeared as SRC Research Report 39 and,in a shortened form,in ACM Transactions on Computer Systems 8,1 (February 1990),18-36.]]

Digital Library

[6]

Ulf Carlsen.Optimal privacy and authentication on a portable communications system.Operating Systems Review,28(3):16 -23,1994.]]

Digital Library

[7]

J.Lawrence Carte and Mark N.Wegman.Universal classes of hash functions.Journal of Computer and System Sciences,18:143 -54,1979.]]

[8]

D.Dolev and A.Yao.On the secu ity of public-key p otocols.IEEE Transactions on Information Theory, 29:198 -208,1983.]]

[9]

W.Feller.An Introduction to Probability Theory and its Applications .John Wiley and Sons,Inc.,New York,1958.]]

[10]

Joshua D.Guttman and F.Javier Thayer Fabrega. P otocol independence through disjoint enc yption.In Proceedings,13th Computer Security Foundations Workshop .IEEE Computer Society Press,July 2000.]]

Digital Library

[11]

Joshua D.Guttman and F.Javier Thayer Fabrega. Authentication tests and the structure of bundles. Theoretical Computer S ience,2001.To appear.]]

Digital Library

[12]

James Heather,Gavin Lowe,and Steve Schneider. Howtopeventtype .awattacksonsecuity p otocols.In Proceedings,13th Computer Security Foundations Workshop .IEEE Compute Society Press,July 2000.]]

Digital Library

[13]

Gavin Lowe.B eaking and .xing the Needham-Schroede public-key protocol using FDR. In Proceeedings of tacas volume 1055 of Lecture Notes in Computer Science,pages 147 -166.Sp inger Verlag,1996.]]

Digital Library

[14]

Gavin Lowe.A hierarchy of authentication speci .cations.In 10th Computer Se urity Foundations Workshop Proceedings,pages 31 -43.IEEE Computer Society Press,1997.]]

Digital Library

[15]

Catherine Meadows.A model of computation for the NRL protocol analyzer.In Proceedings of the Computer Security Foundations Workshop VII,pages 84 -89.IEEE,IEEE Computer Society Press,1994.]]

[16]

Jonathan K.Millen.The Interrogator model.In Proceedings of the 1995 IEEE Symposium on Se urity and Privacy,pages 251 -60,1995.]]

Digital Library

[17]

D.Otway and O.Rees.E .cient and timely mutual authentication.Operating Systems Review,21(1):8 -10, January 1987.]]

Digital Library

[18]

Lawrence C.Paulson.Proving properties of secu ity protocols by induction.In 10th IEEE Computer Security Foundations Workshop,pages 70 -83.IEEE Computer Society Press,1997.]]

Digital Library

[19]

Adrian Perrig and Dawn Xiaodong Song.Looking fo diamonds in the desert:Extending automatic protocol generation to three-party authentication and key agreement protocols.In Proceedings of the 13th IEEE Computer Security Foundations Workshop .IEEE Computer Society Press,July 2000.]]

Digital Library

[20]

Birgit P .tzmann,Matthias Schunter,and Michael Waidner.C yptog aphic security of eactive systems. Ele troni Notes in Theoreti al Computer Science,32, 2000.]]

[21]

Steve Schneider.Verifying authentication p otocols with CSP.In Proceedings of the 10th IEEE Computer Security Foundations Workshop,pages 3 -17.IEEE Computer Society Press,1997.]]

Digital Library

[22]

F.Javier Thayer Fabrega,Jonathan C.Herzog,and Joshua D.Guttman.Strand spaces:P oving security p otocols correct.Journal of Computer Se urity, 7(2/3):191 -230,1999.]]

Digital Library

[23]

Mark N.Wegman and J.Lawrence Carter.New hash functions and thei use in authentication and set equality.Journal of Computer and System Sciences, 22:265 -79,1981.]]

[24]

Thomas Y.C.Woo and Simon S.Lam.Verifying authentication p otocols:Methodology and example. In Pro .Int.Conference on Network Proto ols, Octobe 1993.]]

Cited By

Carbone MHonda KYoshida N(2012)Structured Communication-Centered Programming for Web ServicesACM Transactions on Programming Languages and Systems10.1145/2220365.222036734:2(1-78)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2220365.2220367
Backes MCervesato IJaggard AScedrov ATsay J(2011)Cryptographically sound security proofs for basic and public-key KerberosInternational Journal of Information Security10.1007/s10207-011-0125-610:2(107-134)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1007/s10207-011-0125-6
Adão PBana GHerzog JScedrov A(2009)Soundness and completeness of formal encryption: The cases of key cycles and partial information leakageJournal of Computer Security10.5555/1662658.166266517:5(737-797)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.5555/1662658.1662665
Show More Cited By

Index Terms

The faithfulness of abstract protocol analysis: message authentication

Recommendations

The faithfulness of abstract protocol analysis: message authentication
Special issue on ACM conference on computer and communications security, 2001

Dolev and Yao initiated an approach to studying cryptographic protocols which abstracts from possible problems with the cryptography so as to focus on the structural aspects of the protocol. Recent work in this framework has developed easily applicable ...
An Efficient Deniable Key Exchange Protocol (Extended Abstract)
Financial Cryptography and Data Security

A deniable key exchange allows two parties to jointly share a secret key while neither of two nor an outsider can prove to a third party that the communication between the two happened. This is an important mechanism for realizing a deniably secure ...
An efficient certified email protocol
ISC'07: Proceedings of the 10th international conference on Information Security

A certified email protocol, also known as a nonrepudiation protocol, allows a message to be exchanged for an acknowledgement of reception in a fair manner: a sender Alice sends a message to a receiver Bob if and only if Alice receives a receipt from ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '01: Proceedings of the 8th ACM conference on Computer and Communications Security

November 2001

274 pages

ISBN:1581133855

DOI:10.1145/501983

Conference Chair:
Mike Reiter
Bell Labs, USA
,
Editor:
Pierangela Samarati
University of Milan, Italy

Copyright © 2001 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

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 November 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

CCS01

Sponsor:

SIGSAC

CCS01: 8th ACM Conference on Computer and Communications Security

November 5 - 8, 2001

PA, Philadelphia, USA

Acceptance Rates

CCS '01 Paper Acceptance Rate 27 of 153 submissions, 18%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

26
Total Citations
View Citations
489
Total Downloads

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

Reflects downloads up to 26 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Carbone MHonda KYoshida N(2012)Structured Communication-Centered Programming for Web ServicesACM Transactions on Programming Languages and Systems10.1145/2220365.222036734:2(1-78)Online publication date: 1-Jun-2012
https://dl.acm.org/doi/10.1145/2220365.2220367
Backes MCervesato IJaggard AScedrov ATsay J(2011)Cryptographically sound security proofs for basic and public-key KerberosInternational Journal of Information Security10.1007/s10207-011-0125-610:2(107-134)Online publication date: 1-Jun-2011
https://dl.acm.org/doi/10.1007/s10207-011-0125-6
Adão PBana GHerzog JScedrov A(2009)Soundness and completeness of formal encryption: The cases of key cycles and partial information leakageJournal of Computer Security10.5555/1662658.166266517:5(737-797)Online publication date: 1-Oct-2009
https://dl.acm.org/doi/10.5555/1662658.1662665
Bana GHasebe KOkada M(2009)Computational Semantics for First-Order Logical Analysis of Cryptographic ProtocolsFormal to Practical Security10.1007/978-3-642-02002-5_3(33-56)Online publication date: 14-May-2009
https://dl.acm.org/doi/10.1007/978-3-642-02002-5_3
Tšahhirov ILaud P(2008)Application of Dependency Graphs to Security Protocol AnalysisTrustworthy Global Computing10.1007/978-3-540-78663-4_20(294-311)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78663-4_20
Tšahhirov ILaud P(2007)Application of dependency graphs to security protocol analysisProceedings of the 3rd conference on Trustworthy global computing10.5555/1793574.1793596(294-311)Online publication date: 5-Nov-2007
https://dl.acm.org/doi/10.5555/1793574.1793596
Carbone MHonda KYoshida N(2007)Structured communication-centred programming for web servicesProceedings of the 16th European Symposium on Programming10.5555/1762174.1762178(2-17)Online publication date: 24-Mar-2007
https://dl.acm.org/doi/10.5555/1762174.1762178
Carbone MHonda KYoshida N(2007)A Calculus of Global Interaction based on Session TypesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2006.12.041171:3(127-151)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.1016/j.entcs.2006.12.041
Carbone MHonda KYoshida N(2007)Structured Communication-Centred Programming for Web ServicesProgramming Languages and Systems10.1007/978-3-540-71316-6_2(2-17)Online publication date: 2007
https://doi.org/10.1007/978-3-540-71316-6_2
Bana GMohassel PStegers T(2006)Computational soundness of formal indistinguishability and static equivalenceProceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues10.5555/1782734.1782748(182-196)Online publication date: 6-Dec-2006
https://dl.acm.org/doi/10.5555/1782734.1782748
Show More Cited By

View Options

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