Stepwise development of security protocols: a speech act-oriented approach

ABSTRACT

We propose a novel multi-layers paradigm for the design of key exchange protocols. In the top layer, protocols are specified in a high-level, declarative, formal language using speech acts as the basic building blocks. The declarative semantics of speech acts are specified by their preconditions and effects like in Hoare logics. A protocol logic, called ProtoLog, is developed for reasoning about speech act oriented protocols. Using the language of speech acts, protocol designers could develop their protocols in an modular and compositional way that are correct from the outset.

High-level speech act-oriented protocols are automatically translated into lower-level message exchanging protocols by a "protocol compiler" that implements speech acts by sending and receiving appropriate encrypted messages.

To demonstrate the applicability of our idea, we apply it on the class of well-designed key exchange protocols where a protocol is well-designed if a speech act is executed only if its preconditions are satisfied. We develop a "protocol compiler" for the class of well-designed protocols and prove the soundness and a limited form of completeness of the protocol logic ProtoLog wrt the translation, implemented by the compiler, under the Dolev-Yao assumption of perfect cryptography. An immediate corollary from the soundness result is the guarantee of the secrecy of exchanged keys (an essential security requirement of key exchange protocols) in well-designed protocols.

REFERENCES

• 1: Martín Abadi, Secrecy by typing in security protocols, Journal of the ACM (JACM), v.46 n.5, p.749-786, Sept. 1999 [doi>10.1145/324133.324266]
• 2: Martín Abadi , Roger Needham, Prudent Engineering Practice for Cryptographic Protocols, IEEE Transactions on Software Engineering, v.22 n.1, p.6-15, January 1996 [doi>10.1109/32.481513]
• 3: G. Bella, F. Massacci, L.C. Paulson Verifying the SET registration protocol, IEEE, Journal on selected areas in communication 21, 1, 2003
• 4: G. Bella, F. Massacci, L.C. Paulson An overview of the verification of SET, International J. of Information security, in Press
• 5: Colin Boyd , Wenbo Mao, Designing Secure Key Exchange Protocols, Proceedings of the Third European Symposium on Research in Computer Security, p.93-105, November 07-09, 1994
• 6: 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]
• 7: L. Buttyán, A Simple Logic for Authentication Protocol Design, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.153, June 09-11, 1998
• 8: J. Clark, J. Jakob. A survey of authentication protocol literature, version 1, Department of Computer Science, University of York, Nov 1997
• 9: A. Datta, A. Derek, J. Mitchell, D. Pavlovic A derivation system for security protocols and its logical formalization, IEEE Computer Security Foundation Workshop, 2003
• 10: T. Dierks, C. Allen The TLS protocol version 1.0, RFC 2246, January 1999
• 11: F. J.T. Fabrega, J.C. Herzog, J.D. Guttman. Strand spaces: Why is a security protocol correct ? Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp 160--171, 1998, IEEE Computer Scociety Press
• 12: Ronald Fagin , Joseph Y. Halpern , Moshe Y. Vardi , Yoram Moses, Reasoning about knowledge, MIT Press, Cambridge, MA, 1995
• 13: Joshua D. Guttman, Security Protocol Design via Authentication Tests, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.92, June 24-26, 2002
• 14: 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]
• 15: L. Gong, P. Syverson. Fail-stop protocols: An approavch to designing secure protocols, Proceedings of teh 5th International Conference on Dependable Computing for Critical Applications, 1995, pp 44--55
• 16: 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
• 17: G.E. Hughes, M.J. Cresswell. An introduction to modal logic, Methuen, London and NewYork, 1985
• 18: Yannis Labrou , Tim Finin , Yun Peng, Agent Communication Languages: The Current Landscape, IEEE Intelligent Systems, v.14 n.2, p.45-52, March 1999 [doi>10.1109/5254.757631]
• 19: Gavin Lowe, An attack on the Needham-Schroeder public-key authentication protocol, Information Processing Letters, v.56 n.3, p.131-133, Nov. 10, 1995 [doi>10.1016/0020-0190(95)00144-2]
• 20: Larry Loeb, Secure electronic transactions: introduction and technical reference, Artech House, Inc., Norwood, MA, 1998
• 21: Catherine Meadows, Formal Verification of Cryptographic Protocols: A Survey, Proceedings of the 4th International Conference on the Theory and Applications of Cryptology: Advances in Cryptology, p.135-150, November 28-December 01, 1994
• 22: J. Mitchell, V. Schmatikov, U. Stern Finite State Analysis of SSL 3.0, 7th Usenix Security Symposium, 1998
• 23: Lawrence C. Paulson, Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security (TISSEC), v.2 n.3, p.332-351, Aug. 1999 [doi>10.1145/322510.322530]
• 24: 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
• 25: P. Syverson. Towards a strand semantics for authentication logic, Electronic Notes in Theoretical Computer Science, 20,2000
• 26: Paul Syverson , Catherine Meadows, A Formal Language for Cryptographic Protocol Requirements, Designs, Codes and Cryptography, v.7 n.1-2, p.27-59, Jan. 1996 [doi>10.1007/BF00125075]
• 27: Paul F. Syverson , Paul C. Van Oorschot, On Unifying Some Cryptographic Protocol Logics, Proceedings of the 1994 IEEE Symposium on Security and Privacy, p.14, May 16-18, 1994
• 28: Dawn Xiaodong Song, Athena: a New Efficient Automatic Checker for Security Protocol Analysis, Proceedings of the 1999 IEEE Computer Security Foundations Workshop, p.192, June 28-30, 1999
• 29: D. Wagner, B. Schneier Analysisof the SSL 3.0 protocol, In 2nd Usenix workshop on electronic commerce, 1996

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Logics of programs

General Terms:
Design, Languages, Security, Verification

Keywords:
cryptographic protocols, security protocols