[TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)
Shin'ichiro Matsuo <matsuo@mac.com> Thu, 25 February 2016 16:06 UTC
Return-Path: <matsuo@mac.com>
X-Original-To: tls@ietfa.amsl.com
Delivered-To: tls@ietfa.amsl.com
Received: from localhost (ietfa.amsl.com [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 2AE101B2C15 for <tls@ietfa.amsl.com>; Thu, 25 Feb 2016 08:06:06 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: 0.069
X-Spam-Level:
X-Spam-Status: No, score=0.069 tagged_above=-999 required=5 tests=[BAYES_20=-0.001, FREEMAIL_FROM=0.001, RCVD_IN_DNSWL_LOW=-0.7, RCVD_IN_SORBS_WEB=0.77, SPF_PASS=-0.001] autolearn=ham
Received: from mail.ietf.org ([4.31.198.44]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id Xc1ewOOTZmFN for <tls@ietfa.amsl.com>; Thu, 25 Feb 2016 08:06:04 -0800 (PST)
Received: from st11p02im-asmtp001.me.com (st11p02im-asmtp001.me.com [17.172.220.113]) (using TLSv1.2 with cipher DHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id D98151B2BFC for <tls@ietf.org>; Thu, 25 Feb 2016 08:06:03 -0800 (PST)
Received: from 94.9.168.191.isp.timbrasil.com.br (unknown [64.210.40.106]) by st11p02im-asmtp001.me.com (Oracle Communications Messaging Server 7.0.5.36.0 64bit (built Sep 8 2015)) with ESMTPSA id <0O34006YH21YAS30@st11p02im-asmtp001.me.com> for tls@ietf.org; Thu, 25 Feb 2016 16:06:00 +0000 (GMT)
X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-02-25_05:,, signatures=0
X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 spamscore=0 clxscore=1015 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1510270003 definitions=main-1602250226
From: Shin'ichiro Matsuo <matsuo@mac.com>
Content-type: text/plain; charset="utf-8"
Content-transfer-encoding: quoted-printable
Date: Thu, 25 Feb 2016 08:05:58 -0800
Message-id: <DFA61885-27AD-4E64-AFF7-DD395AE4BC82@mac.com>
To: "<tls@ietf.org>" <tls@ietf.org>
MIME-version: 1.0 (Mac OS X Mail 9.1 \(3096.5\))
X-Mailer: Apple Mail (2.3096.5)
Archived-At: <http://mailarchive.ietf.org/arch/msg/tls/NXGYUUXCD2b9WwBRWbvrccjjdyI>
Subject: [TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)
X-BeenThere: tls@ietf.org
X-Mailman-Version: 2.1.15
Precedence: list
List-Id: "This is the mailing list for the Transport Layer Security working group of the IETF." <tls.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/tls>, <mailto:tls-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/tls/>
List-Post: <mailto:tls@ietf.org>
List-Help: <mailto:tls-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/tls>, <mailto:tls-request@ietf.org?subject=subscribe>
X-List-Received-Date: Thu, 25 Feb 2016 16:06:06 -0000
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] Formal Verification of TLS 1.3 Full Handsha… Shin'ichiro Matsuo
- Re: [TLS] Formal Verification of TLS 1.3 Full Han… Ilari Liusvaara
- Re: [TLS] Formal Verification of TLS 1.3 Full Han… Shin'ichiro Matsuo