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.scot...@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
_______________________________________________ TLS mailing list TLS@ietf.org https://www.ietf.org/mailman/listinfo/tls
