Database of Case Studies Achieved Using CADP

Transport Layer Security Protocol

Organisation: Tecnológico de Monterrey, Campus Estado de México, (MEXICO)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Security Protocols.

Period: 2001

Size: 4,000,000 states
22 mu-calculus formulae

Description: The TLS (Transport Layer Security) protocol aims at providing privacy and integrity of information exchanged by a client/server application running over the Internet. TLS is build on the SSL (Secure Socket Layer) protocol, an authentication protocol for client/server applications.

This work describes the analysis of the handshake protocol of TLS. The goal of the handshake protocol is to establish a secure communication channel between a client and a server. Handshake is a procedure whereby client and server authenticate each other. Upon success, both client and server share a master secret, which is used as a disposable encryption key. As long as the master secret is uncompromised, the connection will remain secure.

As a first step, a formal LOTOS description of the TLS protocol is developed, including a client, a server, a spy or intruder, and a model of the underlying communication medium. The spy can intercept any message in the network, and generate new messages based on its initial knowledge and all previously sent messages (the spy listens to all messages in the network). The communication medium is buffered, i.e., more than a single message might be in transit between two nodes.

In a second step, confidentiality and authentication properties are formalised using two schemas of mu-calculus formulae. Confidentiality is analysed by checking the absence of a transition revealing a secret, and authentication is analysed by checking that a transition e1 is necessarily preceded by a transition e2.

Finally, CADP tools are used for compiling the LOTOS description, simulating the execution of the protocol, and verifying confidentiality and authentication. On average, for the largest scenario (about 4,000,000 million states), the verification of a confidentiality property takes about 2 minutes, and the verification of an authentication property takes about 1 minute.

Conclusions: This case study demonstrates the practical usability of CADP and LOTOS for the analysis of security protocols, illustrating the approach on the example of the TLS protocol.

Publications: [Calixto-Monroy-02] Alberto Calixto and Raúl Monroy. "Formal Analysis of TLS". In Roberto Gómez-Cardenas (editor), Proceedings of the 5th International Conference on Principles of Distributed Systems OPODIS'2001 (Manzanillo, Mexico), December, 2001. Studia Informatica Universalis, Special Issue, Volume 2, Number 2, pages 235-249, 2002.
Available on-line at: http://csmc.ephe.sorbonne.fr:8081/Studia/volumes/proceedings-edited-by-s-i-u/vol-2-hs.2/pdf/15-monroy.pdf/download
or from our FTP site in PDF or PostScript
Contact:
Raúl Monroy
Computer Science Department
ITESM, at Estado de México
Carretera al Lago de Guadalupe Km 3.5 Atizapán, 52926, México
Tel: +52 (55) 5864 5555 x 2466
Fax: +52 (55) 5864 5651
E-mail: raulm@itesm.mx



Further remarks: This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page