IETF Logo Mail Archive

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

Ilari Liusvaara <ilariliusvaara@welho.com> Thu, 25 February 2016 20:11 UTC

Return-Path: <ilariliusvaara@welho.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 3165A1B33E2 for <tls@ietfa.amsl.com>; Thu, 25 Feb 2016 12:11:31 -0800 (PST)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.306
X-Spam-Level:
X-Spam-Status: No, score=-1.306 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, J_CHICKENPOX_46=0.6, RP_MATCHES_RCVD=-0.006] autolearn=no
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 IAe1Df5q0sew for <tls@ietfa.amsl.com>; Thu, 25 Feb 2016 12:11:29 -0800 (PST)
Received: from welho-filter2.welho.com (welho-filter2.welho.com [83.102.41.24]) by ietfa.amsl.com (Postfix) with ESMTP id 968D61A1B91 for <tls@ietf.org>; Thu, 25 Feb 2016 12:11:29 -0800 (PST)
Received: from localhost (localhost [127.0.0.1]) by welho-filter2.welho.com (Postfix) with ESMTP id DB0ADCB9; Thu, 25 Feb 2016 22:11:28 +0200 (EET)
X-Virus-Scanned: Debian amavisd-new at pp.htv.fi
Received: from welho-smtp1.welho.com ([IPv6:::ffff:83.102.41.84]) by localhost (welho-filter2.welho.com [::ffff:83.102.41.24]) (amavisd-new, port 10024) with ESMTP id 7sLsr9Tdx3AK; Thu, 25 Feb 2016 22:11:28 +0200 (EET)
Received: from LK-Perkele-V2 (87-100-151-39.bb.dnainternet.fi [87.100.151.39]) (using TLSv1 with cipher ECDHE-RSA-AES256-SHA (256/256 bits)) (No client certificate requested) by welho-smtp1.welho.com (Postfix) with ESMTPSA id 7D02F286; Thu, 25 Feb 2016 22:11:28 +0200 (EET)
Date: Thu, 25 Feb 2016 22:11:24 +0200
From: Ilari Liusvaara <ilariliusvaara@welho.com>
To: Shin'ichiro Matsuo <matsuo@mac.com>
Message-ID: <20160225201124.GB30171@LK-Perkele-V2.elisa-laajakaista.fi>
References: <DFA61885-27AD-4E64-AFF7-DD395AE4BC82@mac.com>
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Disposition: inline
In-Reply-To: <DFA61885-27AD-4E64-AFF7-DD395AE4BC82@mac.com>
User-Agent: Mutt/1.5.24 (2015-08-30)
Sender: ilariliusvaara@welho.com
Archived-At: <http://mailarchive.ietf.org/arch/msg/tls/nJA15b1-dJA8ChKLk-Q2eo2Bgp8>
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: Thu, 25 Feb 2016 20:11:31 -0000

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

v2.23.0 | Report a Bug | By Email