A Formal TLS Handshake Model in LNT

TL;DR

This paper presents a formal model of the TLS handshake in LNT, enabling automated conformance testing of the protocol to identify vulnerabilities and implementation issues.

Contribution

It introduces a formal LNT model of the TLS handshake and demonstrates its use in automated conformance testing for security protocol analysis.

Findings

Initial empirical results show the effectiveness of the model in detecting protocol deviations.

The formal specification facilitates automated testing of cryptographic protocol implementations.

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.