Subject: [TLS] Simplifying the proof

From: Watson Ladd <[email-masked]>
Date: Fri, 22 Aug 2014 12:39:10 -0700

Dear all,
While we now have a multi thousand line computer checkable proof of
the correctness of the handshake with certain extensions, this is
suboptimal in many respects. It's a pain to check, and interaction
with extensions is even more painful, which means that extending it to
all of TLS 1.3 is going to be even more painful.

How can we fix this? Everything goes fine, up until the master-secret
gets use to derive keys, and then the Finished message is sent. The
reason this isn't good is that we want the keys the record layer uses
to be independent of what an attacker saw in the handshake and they
aren't because of the Finished message coming after the Change Cipher
Spec. If we want key confirmation, we should send a key confirmation
value outside the record layer encryption to solve this. We should
also work on defining security properties we want new features to have
and work backwards, instead of going back from a design to determine
the security it actually provides.

Sincerely,
Watson Ladd