Database of Case Studies Achieved Using CADP

Formal Modeling and Analysis of the TLS Handshake Model

Organisation: CONVECS
Graz University of Technology (AUSTRIA)

Method: LNT

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

Domain: Security Protocols

Period: 2018

Size: 965 lines of LNT

Description: As witnessed by recent vulnerabilities, thorough testing of implementations of security protocols is still necessary. TLS (Transport Layer Security) is a widely used security protocol. It defines rules for the communication between client and server, relying on public-key cryptography in order to ensure integrity of exchanged data.

This case study presents a formal LNT model for the TLS handshake, defined according to the draft standard TLS 1.3. The TLS handshake is a crucial part of TLS because it enables a TLS client and server to establish a secure, authenticated communication link. The handshake specification is provided with two state machines representing the behaviour of client and server, respectively. The LNT model of the TLS 1.3 handshake is archived in the model repository of the MARS workshop series.

From this LNT model, test cases are derived automatically with the TESTOR tool. Concretely, TESTOR takes as input an LNT model and a test purpose, and generates a test case, i.e., an LTS describing the interaction between a tester and an SUT (System Under Test), where the tester tries to drive the SUT towards the goal defined by the test purpose. Three test purposes were considered, derived from requirements of the TLS 1.3 draft specification.

These test cases are then input to the TLS Attacker tool, which issues appropriate requests to an actual TLS implementation, providing concrete values where necessary. Because no implementation of the TLS 1.3 standard was available, the OpenSSL implementation of TLS 1.2 was tested, and (expectedly) found to be not conform to the new version.

Conclusions: LNT provides appropriate abstractions to model security protocols. In particular, the disrupt operator proved to be useful.

Publications: [Bozic-Marsso-Mateescu-Wotawa-18] Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa. "A Formal TLS Handshake Model in LNT". Proceedings of the 3rd Workshop on Models for Formal Analysis of Real Systems and the 6th International Workshop on Verification and Program Transformation (MARS/VPT'18), Thessaloniki, Greece, April 2018.
Available on-line from http://eptcs.web.cse.unsw.edu.au/paper.cgi?MARSVPT2018.1
or from http://cadp.inria.fr/publications/Bozic-Marsso-Mateescu-Wotawa-18.html

Contact:
Lina Marsso
Inria - LIG / CONVECS
655, avenue de l'Europe
CS 90051
38334 Montbonnot
FRANCE
Email: Lina.Marsso@inria.fr



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


Last modified: Thu May 2 13:13:54 2019.


Back to the CADP case studies page