A Formal TLS Handshake Model in LNT

Josip Bozic 1 Lina Marsso 2 Radu Mateescu 2 Franz Wotawa 1
1 TU Graz - Graz University of Technology [Graz]
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular basis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specification. Conformance testing checks whether a system behaves according to its specification. Here model-based testing provides several methods for automated detection of shortcomings. The formal specification of a system behavior represents the starting point of the testing process. In this paper, a widely used cryptographic protocol is specified and tested for conformance with a test execution framework. The first empirical results are presented and discussed.
Document type :
Conference papers
MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. 268, pp.1 - 40, 2018, 〈10.4204/EPTCS.268.1〉
Liste complète des métadonnées

Cited literature [20 references]  Display  Hide  Download
https://hal.inria.fr/hal-01779151
Contributor : Radu Mateescu <>
Submitted on : Thursday, April 26, 2018 - 2:14:50 PM
Last modification on : Wednesday, May 2, 2018 - 9:55:52 AM

File

Bozic-Marsso-Mateescu-Wotawa-1...
Files produced by the author(s)

Identifiers

Collections

LIG_SRCPR | UGA | CONVECS | LIG | INRIA | INRIA-RENGRE

Citation

Josip Bozic, Lina Marsso, Radu Mateescu, Franz Wotawa. A Formal TLS Handshake Model in LNT. MARS/VPT 2018 - 3nd Workshop on Models for Formal Analysis of Real Systems and 6th International Workshop on Verification and Program Transformation, Apr 2018, Thessaloniki, Greece. 268, pp.1 - 40, 2018, 〈10.4204/EPTCS.268.1〉. 〈hal-01779151〉

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

63

Files downloads

10

Contact


archive-ouverte@inria.fr