Related publications: [FJST23]
The paper [FJST23] describes the DTLS(Datagram Transport Layer Security) protocol as a variation of TLS over UDP. It is widely used in wireless networks, and is one of the primary protocols for securing IoT applications. Implementing a state machine for DTLS is complicated by the fact that DTLS’s main challenge is to support the stateless and unreliable transport of UDP, which allows for messages to arrive out of order and/or fragmented. Unsurprisingly, this can result in various subtle implementation bugs.
The paper presents an automated black-box technique for detecting state machine bugs in implementations of stateful network protocols. They have applied their technique on three widely-used implementations of SSH servers and nine different DTLS server and client implementations, including their most recent versions by obtaining their models by model learning. The DTLS server and client models, are in this Benchmark, and the SSH servers models are in the SSH-Fiterau-BrosteanEtAl2023 benchmark. The models are retrieved from the artifact for this paper at [FJST23A].
Also see the SSH-Fiterau-BrosteanEtAl2020 benchmark where older versions of DTLS server and client models are learned.