sofiaceli, Jonathan Hoyland, douglasstebila and me.
Once upon a time...
<div class="t-container">
<div class="r-stack col">
<div class="mermaid">
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
</div>
<div class="fragment mermaid" style="background: #fff">
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
</div>
</div>
<div class="col" >
<ul>
<li>Ephemeral KEM key exchange</li>
<li>KEM public key in certificate</li>
<li>Avoid extra round-trip by letting client send data immediately</li>
</ul>
</div>
</div>
<p class="fragment">Both proofs have seen several corrections, and live in similar, but slightly separate models.</p>
<p>
Tamarin models protocols as <em>rules</em> that take in a set of <em>variables</em> and one or more <em>messages</em>, and then emit new variables and messages.
</p>
<p class="fragment">The (Dolev-Yao) attacker controls the network and can read, send, change, drop all messages.
</p>
<p class="fragment">
Any cryptographic operation is <em>perfect</em>.
Cryptographic compromise is modeled through manually modeled "oracles" that reveal specific keys.
</p>
rule ProtocolMessageI:
[
In(message), VariableI(x)
]
--[
ReceivedMessageFact(message, x)
]->
[
Out(SomeOtherMessage),
VariableII(operation(x))
]
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
"
<div class="col">
<h3>Approach #2</h3>
Build a new model from scratch
</div>
<div class="t-container">
<div class="col">
<h3>Approach #1</h3>
<ol>
<li>Take the <a href="https://tls13tamarin.github.io">TLS 1.3 Tamarin model by Cremers et al.</a></li>
<li>Change it to represent KEMTLS(-PDK)</li>
<li>???</li>
<li>Prove it!</li>
</ol>
</div>
<div class="col">
<h3>Approach #2</h3>
<ol>
<li>Simplify the protocol to its cryptographic core</li>
<li>Convert the pen-and-paper claimed security properties to Tamarin</li>
<li>???</li>
<li>Prove it</li>
</ol>
</div>
</div>
</section>
<section style="font-size: 80%">
<h2>Motivations</h2>
<div class="t-container">
<div class="col">
<h3>Approach #1</h3>
<ol>
<li>Tried-and-tested TLS model</li>
<li>Many tedious protocol details already modeled:
<ul>
<li>Key derivation</li>
<li>Handshake encryption</li>
<li>Message syntax</li>
<li>Record layer</li>
<li>Certificate PKI</li>
</ul>
</li>
<li>Many existing lemmas: both security lemmas as well as "helper" lemmas</li>
</ol>
</div>
<div class="col">
<h3>Approach #2</h3>
<ul>
<li>Precisely model the different levels of forward-secrecy and explicit authentication properties claimed in our pen-and-paper proofs</li>
<li>Don't carry around the baggage of handshake encryption, full TLS key schedule</li>
<li>Analyze KEMTLS' deniability features</li>
</ul>
</div>
</div>
</section>
<section style="font-size: 60%">
<h2>Feature comparison</h2>
<table>
<thead>
<tr>
<th>Feature</th>
<th>Model #1</th>
<th>Model #2</th>
</tr>
<tr>
<th colspan="3"><em>Protocol modelling</em></th>
</tr>
</thead>
<tbody>
<tr>
<td>Encrypted handshake messages</td>
<td>✅</td>
<td>❌</td>
</tr>
<tr>
<td>HKDF and HMAC decomposed into hash</td>
<td>✅</td>
<td>❌</td>
</tr>
<tr>
<td>Key exchange and auth KEMs are same algorithm</td>
<td>✅</td>
<td>❌</td>
</tr>
<tr>
<th colspan="3"><em>Security properties</em></th>
</tr>
<tr>
<td>Adversary can reveal long-term keys</td>
<td>✅</td>
<td>✅</td>
</tr>
<tr>
<td>Adversary can reveal ephemeral keys</td>
<td>✅</td>
<td>❌</td>
</tr>
<tr>
<td>Adversary can reveal intermediate session keys</td>
<td>❌</td>
<td>✅</td>
</tr>
<tr>
<td>Secrecy of handshake and traffic keys</td>
<td>✅</td>
<td>✅</td>
</tr>
<tr>
<td>Forward Secrecy</td>
<td>✅</td>
<td>✅</td>
</tr>
<tr>
<td>Multiple flavours of forward secrecy</td>
<td>❌</td>
<td>✅</td>
</tr>
<tr>
<td>Explicit authentication</td>
<td>✅</td>
<td>✅</td>
</tr>
<tr>
<td>Deniability</td>
<td>❌</td>
<td>✅</td>
</tr>
</tbody>
</table>
</section>
<section style="font-size: 80%">
<h2>Results</h2>
<div class="t-container">
<div class="col">
<h3>Approach #1</h3>
<ul>
<li>Managed to make the model auto-prove
<ul><li style="color: grey; font-size: 50%">We did disable some features not immediately relevant to KEMTLS (including post-handshake authentication, PSK)</li></ul>
</li>
<li>Run-time: 28 hours (many, many cores)</li>
<li>Memory required: >120GB of RAM</li>
<li>Found a minor bug in a lemma of the Cremers et al. model</li>
</ul>
</div>
<div class="col">
<h3>Approach #2</h3>
<ul>
<li>Found several minor mistakes in stated forward secrecy and authentication properties of KEMTLS and KEMTLS-PDK</li>
<li>Proves most security properties of KEMTLS in <strong>minutes</strong>.</li>
</ul>
</div>
</div>
</section>
<section>
<h2>Some more thoughts on Model #2</h2>
<ul>
<li>Surprisingly straightforward model:
<ul>
<li>Direct translation of security properties to Tamarin</li>
<li>~40 hours of work: much less than for #1</li>
<li>Modeling in both instances done by "newbies"</li>
<li>0 helper lemmas (no <code>[reuse]</code>!)</li>
<li>Everything auto-proves</li>
</ul>
</li>
<li>Maybe Tamarin is not so scary after all?</li>
</ul>
</section>
Model your own protocols!
<p class="fragment">Thanks for your attention</p>
<p style="font-family: monospace; font-size: 80%">🐦 <a href="https://twitter.com/thomwiggers">@thomwiggers</a></p>