A tale of two models:

Formal analysis of KEMTLS in Tamarin

Sofía Celi, Jonathan Hoyland, Douglas Stebila and Thom Wiggers.

Once upon a time...

Observation: PQ signatures are quite big and/or slow
Idea: Use KEMs for authentication
Proposal: KEMTLS

KEMTLS

sequenceDiagram Client->>+Server: ClientHello: ephemeral kex Server->>-Client: ServerHello: ephemeral kex Server->>+Client: Certificate: static KEM pk Client->>-Server: Ciphertext Client->>Server: ClientFinished rect rgba(0, 0, 0, 0) Client-->>Server: Application Data end Server->>Client: ServerFinished Server-->>Client: Application Data

sequenceDiagram Client->>+Server: ClientHello: ephemeral kex Server->>-Client: ServerHello: ephemeral kex Server->>+Client: Certificate: static KEM pk Client->>-Server: Ciphertext Client->>Server: ClientFinished rect pink Client-->>Server: Application Data end Server->>Client: ServerFinished Server-->>Client: Application Data

Ephemeral KEM key exchange
KEM public key in certificate
Avoid extra round-trip by letting client send data immediately

KEMTLS variants

Mutual authentication
What if the client already knows the server's public key?
- E.g. resumption, or PSK-like hardcoded keys
- KEMTLS-PDK: KEMTLS with Pre-Distributed Keys

Pen-and-paper proofs

Original KEMTLS paper
- Server-to-client authentication
KEMTLS-PDK paper:
- Server-to-client authentication
- Mutual authentication

Both proofs have seen several corrections, and live in similar, but slightly separate models.

Computer-aided proofs

Proving things by hand:
- Tedious, error-prone work
- Very easy to subconciously fill in gaps in the analysis in your mind
- Very hard to consider many variant protocols together
Computers:
- Very, very good at being very, very literal
- Will not accept handwavyness
- Have no problem keeping track of different protocol variants

Protocol analysis of TLS 1.3

TLS 1.3 has seen lots of pen-and-paper and computer-aided analysis work
Including analyses in Tamarin (Cremers et al.), Proverif (Barghavan et al.)
TLS 1.3 was developed using a "design-break-fix-release" cycle rather than "design-release-break-patch" cycle (Paterson and Van der Merwe)

Tamarin

Tamarin models protocols as rules that take in a set of variables and one or more messages, and then emit new variables and messages.

The (Dolev-Yao) attacker controls the network and can read, send, change, drop all messages.

Any cryptographic operation is perfect. Cryptographic compromise is modeled through manually modeled "oracles" that reveal specific keys.

Tamarin rules


      rule ProtocolMessageI:
        [
          In(message), VariableI(x)
        ]
        --[
          ReceivedMessageFact(message, x)
        ]->
        [
          Out(SomeOtherMessage),
          VariableII(operation(x))
        ]

Tamarin Lemmas


      lemma my_lemma:
        "All key #i #j.
          ExchangedKey(key)@#i  // some protocol-emitted fact
                                // over `key` at time #i
          & K(key)@#j           // Adversary knows `key` at #j
          ==> /* then */
          /* exists a time #z */
          Ex #z.
            /* at which key was revealed */
            RevealedKey(key)@#z
            /* and #z was before #j */
            & #z < #j
        "

Two approaches

Approach #1

Take an existing model and adapt it to represent KEMTLS

Approach #2

Build a new model from scratch

Game plan

Approach #1

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

Approach #2

Simplify the protocol to its cryptographic core
Convert the pen-and-paper claimed security properties to Tamarin
???
Prove it

Motivations

Approach #1

Tried-and-tested TLS model
Many tedious protocol details already modeled:
- Key derivation
- Handshake encryption
- Message syntax
- Record layer
- Certificate PKI
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

Feature comparison

Feature	Model #1	Model #2
Protocol modelling
Encrypted handshake messages	✅	❌
HKDF and HMAC decomposed into hash	✅	❌
Key exchange and auth KEMs are same algorithm	✅	❌
Security properties
Adversary can reveal long-term keys	✅	✅
Adversary can reveal ephemeral keys	✅	❌
Adversary can reveal intermediate session keys	❌	✅
Secrecy of handshake and traffic keys	✅	✅
Forward Secrecy	✅	✅
Multiple flavours of forward secrecy	❌	✅
Explicit authentication	✅	✅
Deniability	❌	✅

Results

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.

Some more thoughts on Model #2

Surprisingly straightforward model:
- Direct translation of security properties to Tamarin
- ~40 hours of work: much less than for #1
- Modeling in both instances done by "newbies"
- 0 helper lemmas (no [reuse]!)
- Everything auto-proves
Maybe Tamarin is not so scary after all?

Wrap-up

A tale of two models: formal analysis of KEMTLS in Tamarin

Two approaches, two viewpoints: more confidence
It is possible to rigorize your pen-and-paper proofs in Tamarin
Full version of the paper and model source code available at https://kemtls.org/.

Model your own protocols!

Thanks for your attention

🐦 @thomwiggers