Not-quite-so-broken TLS 1.3 mechanised conformance checking. David Kaloper-Meršinjak and Hannes Mehnert. In TRON workshop, 2016. [ bib | pdf ]
We present a set of tools to aid TLS 1.3 implementors, all derived from a single TLS implementation/model. These include an automated offline TLS protocol conformance checker, a test oracle validating recorded sessions, a tool replicating recorded sessions with other implementations, and an interactive online handshake visualisation.

The conformance checker repeatedly runs a user-provided TLS implementation, attempting to establish TLS sessions with it; the checker explores the TLS parameter space to determine feature coverage of the provided implementation. The test oracle takes a recorded session between two endpoints and decides whether the session was conformant with the specification. The replication utility re-runs one side of a recorded session against another TLS implementation, and observes its behaviour. The online visualisation accepts connections from clients and presents the TLS session as an interactive sequence diagram.

All of these tools are based on our clean-slate nqsb-TLS implementation/model. It already supports TLS 1.0-1.2, and interoperates with a broad range of other TLS implementations. We are currently extending nqsb-TLS with TLS 1.3 support, and tracking the progress of the TLS 1.3 draft, adapting our implementation/model accordingly.

We invite the community to use our tools while implementing the TLS 1.3 RFC, and provide feedback on deviations in the interpretation thereof. This process enables the community to converge to a single, mechanically checkable TLS 1.3 model, as implemented by nqsb-TLS.