Overview
Attached are the Mealy machine models for each implementation. A few things to note:
- JSSE models are significantly larger (100 states) than the rest. Some PionDTLS models are pretty large as well.
- the name of the model encodes the alphabet (how many key exchange algorithms were included) and the certificate configuration. 'all' means all 4 key exchange (rsa, psk, ecdh, dh) algorithms. The more key exchange algorithms are used, the larger the input alphabet.
- models were generated using model learning with abstraction implemented via Mapper component. For more details, check DTLS server paper.
- models were tested using an adaptation of Random Walk which starts from an arbitrarily chosen state
- the Scandium ECDH and NSS models omit retransmissions w.r.t. the message suequence and epoch numbers. All others include these retransmissions.
Contiki-NG TinyDTLS
ctinydtls_ecdhe_cert_none.dot
ctinydtls_ecdhe_cert_req.dot
ctinydtls_psk.dot
Eclipse TinyDTLS
etinydtls_ecdhe_cert_none.dot
etinydtls_ecdhe_cert_req.dot
etinydtls_psk.dot
GnuTLS (multiple versions)
gnutls-3.5.19_psk_rsa_cert_nreq.dot
gnutls-3.6.7_all_cert_none.dot
gnutls-3.6.7_all_cert_nreq.dot
gnutls-3.6.7_all_cert_req.dot
JSSE (reference Java DTLS implementation)
jsse-12_rsa_cert_none.dot
jsse-12_rsa_cert_nreq.dot
jsse-12_rsa_cert_req.dot
MbedTLS (version 2.16.1)
mbedtls_all_cert_none.dot
mbedtls_all_cert_nreq.dot
mbedtls_all_cert_req.dot
NSS
nss-3.6.7_dhe_ecdhe_rsa.dot
OpenSSL
openssl-1.1.1b_all_cert_none_nreq.dot
openssl-1.1.1b_all_cert_nreq.dot
openssl-1.1.1b_all_cert_req.dot
PionDTLS
pion_ecdhe_cert_none.dot
pion_ecdhe_cert_nreq.dot
pion_ecdhe_cert_req.dot
pion_psk.dot
Scandium
scandium-2.0.0_ecdhe_cert_none.dot
scandium-2.0.0_ecdhe_cert_nreq.dot
scandium-2.0.0_ecdhe_cert_req.dot
scandium-2.0.0_psk.dot
scandium_latest_ecdhe_cert_none.dot
scandium_latest_ecdhe_cert_nreq.dot
scandium_latest_ecdhe_cert_req.dot
scandium_latest_psk.dot
WolfSSL
wolfssl-4.0.0_dhe_ecdhe_rsa_cert_req.dot
wolfssl-4.0.0_psk.dot
