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

From: Shin'ichiro Matsuo <[email-masked]>
Date: Thu, 25 Feb 2016 08:05:58 -0800

Hi all,

 [Introduction]

CELLOS (Cryptographic protocol Evaluation toward Long-Lived Outstanding Security) forms a team for formal verification of TLS. It has modeled TLS 1.3 draft specification and conducted verification by using ProVerif. Until now, we have modeled the full handshake protocol in draft-06, -09, -10, and -11. As a result of this formal verification, we did not find any security flaw. You can freely download the latest descitption of formal model at

https://www.cellos-consortium.org/studygroup/TLS1.3-fullhandshake-draft11.pv
 
Any comments, advices, requests and modification from TLS experts are welcome for further evaluations. We share the models and verification results.

Our modeling policy is straightforward formalization, that is, we aim to faithfully follow the draft specification. In other words, we did not simplify the protocol (at least at the symbolic level) and all the variables appeared in the draft are included in the formalized model.
On the other hand, the sizes of the variables are not modeled and side-channel attacks (including padding oracle attack) are not taken into account.

 [Target version]
TLS 1.3 draft-11 full handshake protocol

-------------------------------------
[Tool]
ProVerif 1.92
http://prosecco.gforge.inria.fr/personal/bblanche/proverif/

After installing the latest version of ProVerif, run the following command to execute the evaluation.
$ proverif -in pitype TLS1.3-fullhandshake-draft11.pv

[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?

[Evaluation results]
* Secrecy: secure (ProVerif outputs "true")
* Authentication: secure

We did not find an attack against the full handshake protocol in draft-11 in above setting.

[Evaluation environment and evaluation time]
CPU: Intel Core i7-4600U (2.10 GHz)
Memory: 16 GB
OS: Windows 7 (64-bit)
Time: 56 minutes

Regards,
Shin’ichiro Matsuo

---

From: Ilari Liusvaara <[email-masked]>
Date: Thu, 25 Feb 2016 22:11:24 +0200

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