A Formal TLS Handshake Model in LNT
This work addresses cyber security challenges for network service developers, but it appears incremental as it applies existing model-based testing methods to a specific protocol.
The paper tackled the problem of conformance testing for network services by formally specifying and testing a widely used cryptographic protocol, presenting initial empirical results.
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.