Subject: Re: [TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)

From: Shin'ichiro Matsuo <[email-masked]>
Date: Tue, 01 Mar 2016 17:44:30 -0800

Hi Ilari,

Thank you for your kind comments. We will try to commented cases.

Regards,
Shin’ichiro Matsuo

> On Feb 25, 2016, at 12:11 PM, Ilari Liusvaara <[email-masked]> wrote:
> 
> On Thu, Feb 25, 2016 at 08:05:58AM -0800, Shin'ichiro Matsuo wrote:
> 
>> 
>> -------------------------------------
>> 
>> [What's checked]
>> We checked the TLS draft-11 full handshake protocol for the following two properties.
>> * Secrecy of payload: Can the attacker know the encrypted payload?
>> * Authenticity: Can the attacker impersonate the server?
> 
> I think the following should be checked as well (once the relevant
> definitions are available):
> 
> - signed TLS-EXPORTER results can be used for authentication.
> - TLS-EXPORTER results can be used as secure encryption keys.
> 
> There are many pieces of sofware that rely on those two properties.
> 
> 
> Also, reading the .pv file, it seems like only 1-RTT GDHE-CERT mode is
> verified, not GDHE-PSK nor PSK nor any kind of 0-RTT mode.
> 
> (And then there are possibly even worse problems with usage... Not that
> I know what's the "correct" model there).
> 
> 
> 
> -Ilari