|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 |
Back to the CADP case studies page