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-01] 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. 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 the CADP Web site in PDF or PostScript [Calixto-Monroy-02] Alberto Calixto and Raúl Monroy. "TLS Analysis Using CADP". Studia Informatica Universalis, Studia Informatica Universalis, Special Issue, Volume 2, Number 2, pages 235-249, 2002. Available on-line at: http://homepage.cem.itesm.mx/raulm/pub/15-Monroy.pdf or from the CADP Web 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

Back to the CADP case studies page