Re: [TLS] Formal Verification of TLS 1.3 Full Handshake Protocol Using ProVerif (Draft-11)
Shin'ichiro Matsuo <matsuo@mac.com> Wed, 02 March 2016 01:44 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 384C51A8862 for <tls@ietfa.amsl.com>; Tue, 1 Mar 2016 17:44:36 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2
X-Spam-Level:
X-Spam-Status: No, score=-2 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, FREEMAIL_FROM=0.001, J_CHICKENPOX_46=0.6, RCVD_IN_DNSWL_LOW=-0.7, 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 OmL4XglK1vg0 for <tls@ietfa.amsl.com>; Tue, 1 Mar 2016 17:44:35 -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 EBEA91A700C for <tls@ietf.org>; Tue, 1 Mar 2016 17:44:34 -0800 (PST)
Received: from [172.20.10.2] (51.sub-70-213-0.myvzw.com [70.213.0.51]) by st11p02im-asmtp001.me.com (Oracle Communications Messaging Server 7.0.5.36.0 64bit (built Sep 8 2015)) with ESMTPSA id <0O3E01D1Y2672A30@st11p02im-asmtp001.me.com> for tls@ietf.org; Wed, 02 Mar 2016 01:44:34 +0000 (GMT)
X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2016-03-01_11:,, signatures=0
X-Proofpoint-Spam-Details: rule=notspam policy=default score=0 spamscore=0 clxscore=1011 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-1603020031
Content-type: text/plain; charset="utf-8"
MIME-version: 1.0 (Mac OS X Mail 9.1 \(3096.5\))
From: Shin'ichiro Matsuo <matsuo@mac.com>
In-reply-to: <20160225201124.GB30171@LK-Perkele-V2.elisa-laajakaista.fi>
Date: Tue, 01 Mar 2016 17:44:30 -0800
Content-transfer-encoding: quoted-printable
Message-id: <F9F3CF29-0E52-475A-9EDB-6746DDACB25C@mac.com>
References: <DFA61885-27AD-4E64-AFF7-DD395AE4BC82@mac.com> <20160225201124.GB30171@LK-Perkele-V2.elisa-laajakaista.fi>
To: Ilari Liusvaara <ilariliusvaara@welho.com>
X-Mailer: Apple Mail (2.3096.5)
Archived-At: <http://mailarchive.ietf.org/arch/msg/tls/Fuk-rIiHlEhOZfmoLRs0i3j4Vvc>
Cc: "<tls@ietf.org>" <tls@ietf.org>
Subject: Re: [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: Wed, 02 Mar 2016 01:44:36 -0000
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 <ilariliusvaara@welho.com> 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
- [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