A Formal TLS Handshake Model in LNT

Josip Bozic, Lina Marsso, Radu Mateescu, and Franz Wotawa

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 2018, Thessaloniki, Greece, April 2018

Abstract:

Testing of network services represents one of the biggest challenges in cyber security. Because new vulnerabilities are detected on a regular ba- sis, more research is needed. These faults have their roots in the software development cycle or because of intrinsic leaks in the system specifica- tion. 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.

40 pages

PDF

PostScript

Slides of J. Bozic's lecture at the MARS'18 workshop

PDF

(slides prepared together with L. Marsso and R. Mateescu)