Automatic verification of the TLS handshake protocol

ABSTRACT

E-commerce is based on transactions between client and server agents. These transactions require a protocol that provides privacy and reliability between these two agents. A widely used protocol on e-commerce is Transport Layer Security (TLS). In this paper we present a way to use Formal Methods to ensure the e-commerce properties of this protocol. Specifically we use a known tool for Model Checking (UPPAAL) to describe and analyze the behaviour of the protocol (by means of timed automata). Thus, with this tool we can make an automatic verification of TLS.

REFERENCES

• 1: J. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, Yi Wang, and C. Weise, New Generation of UPPAAL, Int. Workshop on Software Tools for Technology Transfer, June 1998.
• 2: Dominique Bolignano, Towards the Formal Verification of Electronic Commerce Protocols, Proceedings of the 10th Computer Security Foundations Workshop (CSFW '97), p.133, June 10-12, 1997
• 3: Philippa Broadfoot and Gavin Lowe, On distributed security transactions that use secure transport protocols, 2003.
• 4: G. Díaz, D. Cazorla, F. Pelayo, F. Cuartero, and V. Valero, Verifying and capturing probabilistic bechaviours of real-time systems, 19th Annual UK Performance Engineering Workshop, 2003.
• 5: Internet Engineering Task Force, The tls protocol version 1.1, work in progress (June 2003), http://www.ietf.org/internet-drafts/draft-ietf-tls-rfc2246-bis-05.txt.
• 6: K. Larsen, P. Pettersson, and Wang Yi, UPPAAL in a Nutshell, Int. Journal on Software Tools for Technology Transfer 1 (1997), no. 1--2, 134--152.
• 7: K. G. Larsen , F. Larsson , P. Pettersson , W. Yi, Efficient verification of real-time systems: compact data structure and state-space reduction, Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS '97), p.14, December 03-05, 1997
• 8: G. Lowe, Towards a Completeness Result for Model Checking of Security Protocols, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.96, June 09-11, 1998
• 9: A. Roscoe, Proving Security Protocols with Model Checkers by Data Independence Techniques, Proceedings of the 11th IEEE Computer Security Foundations Workshop, p.84, June 09-11, 1998
• 10: P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe, Modelling and analysis of security protocols, Addison Wesley, 2001.

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce

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

  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Keywords:
authentication protocols, authentication protocols and model checking, e-Commerce, security, system verification and model checking