Re: [TLS] Current TLS 1.3 state?

We’re hoping that the TLS:DIV workshop later this month will serve to gather some opinions from the academic community on the current spec.
https://www.mitls.org/tls:div/ <https://www.mitls.org/tls:div/>

At IEEE S&P (Oakland), there will be at least two papers on analyses of draft 18:
- A ProVerif and CryptoVerif analysis of the protocol (and a minimal reference implementation)
- A verified F* implementation of the record layer

So, putting these together with the upcoming Tamarin analysis and previously published papers on prior drafts, I think we’ll have a solid bibliography justifying the core design of TLS 1.3, especially the (EC)DHE and PSK 1-RTT handshakes along with resumption.

What I am less confident about is the secure usage of features like 0-RTT, 0.5 RTT, and post-handshake authentication.
Many researchers have looked at these aspects (and they can correct me if I am wrong) but the security guarantees we can prove for these modes is much more limited than for the regular 1-RTT handshake. My concern is that these features will inspire new usage patterns will emerge for TLS 1.3 that have not been adequately studied. I am not sure what we can do about that except maybe work harder on the security considerations.

-Karthik

> On 5 Apr 2017, at 10:44, Sam Scott <sam.scott89@gmail.com> wrote:
> 
>> I don't know what the state of the various modelling efforts is, though I imagine
>> this will be a topic at TLS:DIV at the end of the month. We did discuss the various
>> cryptographic changes in -20 (specifically the extra key derive stages and the
>> handshake hash reification) with a number of cryptographers before incorporating.
>> Perhaps some of the analytic groups on-list would care to comment?
> 
> From our* point of view we're pretty happy with the current state of the spec.
> Our initial results confirm that TLS achieves the core security properties
> (secrecy and authentication). More specifically, we prove an absence of attacks
> against those properties in our model.
> 
> We're currently waiting for the last version of the spec to be finalised so that
> we can make a more definitive statement and share our final results. Although we
> do not expect our analysis to be affected by the recent changes to the spec, we
> will still need to update our model and re-prove everything, which is quite time
> consuming. We will be talking at TLS:DIV so can share more then, including what
> is and isn't captured by our model.
> 
> * Us being the Tamarin team: Cas Cremers, Marko Horvat, Jonathan Hoyland,
> Sam Scott, and Thyla van der Merwe.
> 
> _______________________________________________
> TLS mailing list
> TLS@ietf.org
> https://www.ietf.org/mailman/listinfo/tls