Learning bankcard with a manual constructed mapper

The Mapper setup

To infer the state machines of implementations of the TLS protocol we used LearnLib, which uses a modified version of Angluin’s L* algorithm. An implementation that is analysed is referred to as the System Under Test (SUT) and is considered to be a black box. LearnLib has to be provided with a list of messages it can send to the SUT (also known as the input alphabet), and a command to reset the SUT to its initial state. A test harness is needed to translate abstract messages from the input alphabet to concrete messages that can be sent to the SUT.

To use LearnLib, we need to fix an input alphabet of messages that can be sent to the SUT. This alphabet is an abstraction of the actual messages sent. In our analyses we use different input alphabets depending on whether we test a client or server, and whether we perform a more limited or more extensive analysis. To test servers we support the following messages: ClientHello (RSA and DHE), Certificate (RSA and empty), ClientKeyExchange, ClientCertificateVerify, ChangeCipherSpec, Finished, ApplicationData (regular and empty), HeartbeatRequest and HeartbeatResponse. To test clients we support the following messages: ServerHello (RSA and DHE), Certificate (RSA and empty), CertificateRequest, ServerKeyExchange, ServerHelloDone, ChangeCipherSpec, Finished, ApplicationData (regular and empty), HeartbeatRequest and HeartbeatResponse.

Learned models of TLS protocols

Below models were learned from real TLS implementations with the learning setup described below.

Pictures of Learned Models

Some of the learned models listed in the table Models of TLS protocols above are shown below :

GnuTLS

PolarSSL

OpenSSL