Graz University of Technology (AUSTRIA)
CADP (Construction and Analysis of Distributed Processes)
965 lines of LNT
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
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.
LNT provides appropriate abstractions to model security protocols. In
particular, the disrupt operator proved to be useful.
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
Inria - LIG / CONVECS
655, avenue de l'Europe
|Further remarks:||This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|