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
