Joshua D. Guttman
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.
- 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.]] Google Scholar
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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]] Google ScholarDigital Library
- 6.Ulf Carlsen.Optimal privacy and authentication on a portable communications system.Operating Systems Review ,28(3):16 -23,1994.]] Google ScholarDigital Library
- 7.J.Lawrence Carte and Mark N.Wegman.Universal classes of hash functions.Journal of Computer and System Sciences ,18:143 -54,1979.]]Google ScholarCross Ref
- 8.D.Dolev and A.Yao.On the secu ity of public-key p otocols.IEEE Transactions on Information Theory , 29:198 -208,1983.]]Google Scholar
- 9.W.Feller.An Introduction to Probability Theory and its Applications .John Wiley and Sons,Inc.,New York,1958.]]Google Scholar
- 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.]] Google ScholarDigital Library
- 11.Joshua D.Guttman and F.Javier Thayer Fabrega. Authentication tests and the structure of bundles. Theoretical Computer S ience ,2001.To appear.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]]Google Scholar
- 16.Jonathan K.Millen.The Interrogator model.In Proceedings of the 1995 IEEE Symposium on Se urity and Privacy ,pages 251 -60,1995.]] Google ScholarDigital Library
- 17.D.Otway and O.Rees.E .cient and timely mutual authentication.Operating Systems Review ,21(1):8 -10, January 1987.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]]Google Scholar
- 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.]] Google ScholarDigital 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.]] Google ScholarDigital 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.]]Google Scholar
- 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.]]Google Scholar
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, 2001Dolev 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 SecurityA 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 SecurityA 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