Approach #1

1. Take the TLS 1.3 Tamarin model by Cremers et al.
2. Change it to represent KEMTLS(-PDK)
3. ???
4. Prove it!

Approach #2

1. Simplify the protocol to its cryptographic core
2. Convert the pen-and-paper claimed security properties to Tamarin
3. ???
4. Prove it

Approach #1

1. Tried-and-tested TLS model
2. Many tedious protocol details already modeled:
   • Key derivation
   • Handshake encryption
   • Message syntax
   • Record layer
   • Certificate PKI
3. Many existing lemmas: both security lemmas as well as "helper" lemmas

Approach #2

• Precisely model the different levels of forward-secrecy and explicit authentication properties claimed in our pen-and-paper proofs
• Don't carry around the baggage of handshake encryption, full TLS key schedule
• Analyze KEMTLS' deniability features

Approach #1

• Managed to make the model auto-prove
  • We did disable some features not immediately relevant to KEMTLS (including post-handshake authentication, PSK)
• Run-time: 28 hours (many, many cores)
• Memory required: >120GB of RAM
• Found a minor bug in a lemma of the Cremers et al. model

Approach #2

• Found several minor mistakes in stated forward secrecy and authentication properties of KEMTLS and KEMTLS-PDK
• Proves most security properties of KEMTLS in minutes.