The faithfulness of abstract protocol analysis: message authentication

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: Martín Abadi , Phillip Rogaway, Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption), Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical Informatics, p.3-22, August 17-19, 2000
• 2: Mihir Bellare, Practice-Oriented Provable-Security, Proceedings of the First International Workshop on Information Security, p.221-231, September 17-19, 1997
• 3: Mihir Bellare , Joe Kilian , Phillip Rogaway, The Security of Cipher Block Chaining, Proceedings of the 14th Annual International Cryptology Conference on Advances in Cryptology, p.341-358, August 21-25, 1994
• 4: Mihir Bellare , Phillip Rogaway, Entity authentication and key distribution, Proceedings of the 13th annual international cryptology conference on Advances in cryptology, p.232-249, January 1994, Santa Barbara, California, United States
• 5: Michael Burrows , Martin Abadi , Roger Needham, A logic of authentication, ACM Transactions on Computer Systems (TOCS), v.8 n.1, p.18-36, Feb. 1990 [doi>10.1145/77648.77649]
• 6: Ulf Carlsen, Optimal privacy and authentication on a portable communications system, ACM SIGOPS Operating Systems Review, v.28 n.3, p.16-23, July 1994 [doi>10.1145/182110.182112]
• 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 , F. Javier Thayer, Protocol Independence through Disjoint Encryption, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.24, July 03-05, 2000
• 11: Joshua D. Guttman , F. Javier Thayer, Authentication tests and the structure of bundles, Theoretical Computer Science, v.283 n.2, p.333-380, June 14, 2002 [doi>10.1016/S0304-3975(01)00139-6]
• 12: James Heather , Gavin Lowe , Steve Schneider, How to Prevent Type Flaw Attacks on Security Protocols, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.255, July 03-05, 2000
• 13: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 14: Gavin Lowe, A Hierarchy of Authentication Specifications, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.31, June 10-12, 1997
• 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: J. K. Millen, The Interrogator model, Proceedings of the 1995 IEEE Symposium on Security and Privacy, p.251, May 08-10, 1995
• 17: Dave Otway , Owen Rees, Efficient and timely mutual authentication, ACM SIGOPS Operating Systems Review, v.21 n.1, p.8-10, Jan. 1987 [doi>10.1145/24592.24594]
• 18: Lawrence C Paulson, Proving Properties of Security Protocols by Induction, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.70, June 10-12, 1997
• 19: A. Perrig , D. Song, Looking for Diamonds in the Desert - Extending Automatic Protocol Generation to Three-Party Authentication and Key Agreement Protocols, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.64, July 03-05, 2000
• 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 protocols with CSP, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.3, June 10-12, 1997
• 22: F. Javier Thayer Fábrega, Strand spaces: proving security protocols correct, Journal of Computer Security, v.7 n.2-3, p.191-230, Jan. 1999
• 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.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Authentication

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Authentication

  E. Data
  E.4 CODING AND INFORMATION THEORY
      Subjects: Formal models of communication

General Terms:
Algorithms, Design, Security