Time
Remote access:
Administrivia
-- chairs, 5 mins
TLS formal analysis
-- Rich Salz or Joe Salowey, 10 mins
Attested TLS
-- Muhammad Usama Sardar, 30 mins
Verifying iMessage
-- Felix Linker, 30 mins
long-promised presentation
-- Jonathan Hoyland, remaining time:-)
AOB
Stephen Farrell greeted the audience
The audience is small, no need for formal queueing
Joe Salowey talks from the TLS group
They prepare a process for protocol formal reviews
More work to be done, to make this smooth and efficient
If anyone is interested, should go to the TLS meeting
TLS has the best formal analysis out there
Jonathan Hoyland asks, Joe answers formal analysis triage team
Once the triage team accepts an analysis, then there is no
way to introduce another analysis
Joe answers: we can ease the process
Stephen 2 suggestions: the process is experimental
maybe if that team gives an analysis, please forward it to UFMRG
If an analysis would be too much time, probably UFMRG could tackle it
Jonathan: we have to redo the analysis from scratch
because it breaks some fundamental assumption
It would be painful
Joe: if it's a published draft, it's a problem
What is the incentive to do the analysis?
How long would it take?
What is the estimated effort?
We are happy to analyse, but what is our incentive?
If we are stuck, what is the latency of asking questions
and getting an
Joe: TLS meeting on Friday, we need feedback
collaboration
Jonathan: answering your first question: it gonna be
publish this as a result, as it would not be novel
We might use a UFMRG publication venue
Stephen encourages people to attend the TLS meeting
Colin Perkins
IETF has its own academic journal
Prefers correctness over novelty
Regular paper deadline is April
End of this session
Next: Muhammad Usama Sardar talks about Specifications of Attested TLS
How do we actually write the specifications?
Clearly. That is a lot of help.
Hannes dragt tls attestation
Combining attestation into TLS
work in progress
Pre-handshake
Background: what TLS is: most commonly used protocol
Private Key: TLS identity key, certification authority certifies this
What if the key is leaked? That breaks the security argument.
We need remote attestation.
Attested TLS is the composition of TLS and remote attestation
We must not be repeating what is already there in TLS.
Pre, Post and Intra Handshake.
Jonathan: maybe there is an interleaving as the fourth option
If you think of TLS, one attestation is one round-trip.
Usama:
Attester, verifying party
Two combinations: server is the attester
client is the attester
Server: in addition to TLS nonce, there will be attestation nonce
for post-handshake, TLS handshake has now finished
I need to send a nonce and generate the evidence
extra round-trip
Client: server is the verifying relying party
Needs to request a certificate
Server will ask it
Both pre and intra
Three options: pre-handshake, then TLS happens
intra-handshake: attestation happens within the TLS handshake
post-handshake: TLS handshake, creates evidence, nonce coming from the
server to the client
Design space for attested tls
What is the point of writing this internet draft?
Three options for design for pre-handshake
selfissued, ta issued, ca issued
intra handshake: without negotiation, with negotiation
post-handshake: tls exporters, exported, post-handshake exchange
new draft: how
is there any fundamental design option that is missing here?
Jonathan: the options are very subtle
we'll never be able to prove that it has the same guarantee as TLS
Felix: the critical thing: what are the security requirements?
You can just pick any
Usama: They have different security requirements
Stephen: design space:
which are of the 13 designs easier to prove?
Usama: pre and post are easier, intra is more effort
In the beginning I didn't want intra, but I was convinced it gives
strong binding
Steve Crocker: I like the question, and the response
tree like that, how do you evaluate which one to verify?
can you apply some metrics?
strong idea should be included
making explicit what the metrics are
Usama: tradeoffs slide
Jonathan: when you are combining protocols
first protocol establishes a secret
remote attestation does not establish a common secret
we can't get the authentication property
it's my theory
Usama: simplistic picture
there's a shared secret between the two
we don't want to design from scratch
why don't we compose together
tls and exchange of the evidence
Jonathan: compound authentication
imagine tls is broken
leaked a private key
do we know
suppose attest is broken
key is leaked
do we know whether it was run honestly
Usama: Cedric mentioned the channel binding properties
at hackathon
strong binding: if one is broken, the other protocol should be able to
prove that it's broken
not for pre and post
Usama: Specifications key exchange and authentication part
ra-tls, pre,
tls attest
scone
specifications of the authentication parts
how long the tls identity key
security concerns, how long they live
replay attacks
who is signing the certificate?
Which format? x.509, negotiated
Discussion: is there any design options?
Threat model: non-psk handshake
tls or attestation key leaks
properties of attested tls
tls properties: server authentication
rfc9934 is vague about security considerations
per session evidence freshness
integrity of evidence is protected
work in progress: relay attacks
channel binding properties
credit: Cedric Fournet
Tradeoffs on pre post and intra
summary: underspecified: not trustworthy
end of Usama's session
Felix Linker talks
A formal analysis if apple's iMessage PQ3 protocol
Post Quantum
What we can do with Tamarin
challenging
new state of the art in quantum secure messaging
Level 3 pqc key establishment
ongoing pqc rekeying
example
forward secrecy
post-compromise security
high level of iMessage
... difficult technical description...
more detailed view how this works
iMessage double ratchet construction
How to make this post quantum secure
integrating it to the double ratchet
gets post quantum post compromise security
adversary model
active network adversary perfect crypto assumtion
may obtain quantum computer
harvest now, decrypt later
then protocol execution stops
we cannot defend against an active quantum attacker
goals
understand security goals thoroughly
verify that imessage meets security goals
Bad news: unbounded looping protocols like signal
with mutable recursive data structures are
out of scope for eymbolic provers
Tamarin: multiset rewriting
models what participants can do
equational theory for crypto operations
adversary how it can play
security properties are trace properties
written as lemmas
Tamarin does constraint solving
finds a counterexample: an attack
This is what we did on iMessage
How did we model iMessage?
Setup phase, participants generate the keys
start a session with a fresh session fact
prekeys
ephemeral keys
protocol execution : rules for sending and receiving messages
participants can decide to send or receive
third phase: post quantum phase:
defense against harvest now, decrypt later
Secrecy of iMessage
messages are secure unless four things happen
blue keys leak
chain keys leaked
leaked two kem shared and dh keys
we show secrecy, forward secrecy and post compromise security
Where is the quantum attacker?
It hides how can they learn
DH is for free for them
32 lemmas
2.5 person months of work
Stephen: 2.5 months for somebody experienced in Tamarin
We provide a general proof methodology
Some people said this is not possible with Tamarin
Full details in eprint paper
iacr
Gergely: is looping protocols with mutually recursive data structures a
theoretical limitation or Tamarin's limitation?
Felix: this is not a limitation, we did it
Usama: did you discover some Tamarin limitations?
If somebody unfamiliar with Tamarin, would the person have issues with
this protocol?
Jonathan: what was the specific thing that was considered impossible for
looping protocols? TLS is one
Felix: we have a doubly nested loop of key derivation
When you ask Tamarin,
Jonathan: we used induction
Felix: people used your papers should have come to the conclusion
earlier
End of session of Felix
Stephen: Jonathan's talk is cancelled
Closing