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 _______________________________________________ TLS mailing list [email protected] https://www.ietf.org/mailman/listinfo/tls
