Re: [TLS] Adoption call for draft-rescorla-tls-ctls

Antoine Delignat-Lavaud <antoine@delignat-lavaud.fr> Mon, 25 November 2019 13:49 UTC

Return-Path: <antoine@delignat-lavaud.fr>
X-Original-To: tls@ietfa.amsl.com
Delivered-To: tls@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id CDEA612095E for <tls@ietfa.amsl.com>; Mon, 25 Nov 2019 05:49:51 -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, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=delignat-lavaud.fr
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 NRzI6WHTbLGH for <tls@ietfa.amsl.com>; Mon, 25 Nov 2019 05:49:49 -0800 (PST)
Received: from argon.maxg.info (argon.maxg.info [IPv6:2001:41d0:2:7f22::1]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 0150612095D for <tls@ietf.org>; Mon, 25 Nov 2019 05:49:48 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=delignat-lavaud.fr; s=dkim; h=Message-ID:References:In-Reply-To:Subject:Cc: To:From:Date:Content-Transfer-Encoding:Content-Type:MIME-Version; bh=pttqqabnU4r5Y+yP5j86RSgTstgzv85ATSVHsc50uOw=; b=O3Ayo21RWnXo9xOc+j4VJC9jvs LcntR26rD7p86am5cOvIJiCG15iwvy4U0amJF9tqBlF3FCAFDu9h+Uv5R+oLTB/K7s5DfhnTkeRbx pW57YYNck7fWa1HW3Nf/I0Rr0olaCpkfu1t/KJvO+Wbf73chcX98Fa1eGbH8jIU+nPBjP0aipO1gn 5BGrGZbojeYqT+0gmgPTqw+F9o2iv2r7YxJzc8+hmImWxVNhH9vpfRAXIwXuMeLlWDw0PB/ei+Tmz P05tsNo4i8bXkQVigdstFGL95v7rbjGmuDwfQSW4huT6LHRXPvd4iqOlV4+RHOeAnU3fTskpXpQ0g oPD1h/Og==;
Received: from localhost (authenticated.user.IP.removed [::1]) by argon.maxg.info with esmtpa (envelope-from <antoine@delignat-lavaud.fr>) id 1iZEkM-00024u-Tx ; Mon, 25 Nov 2019 14:49:46 +0100
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
Date: Mon, 25 Nov 2019 13:49:45 +0000
From: Antoine Delignat-Lavaud <antoine@delignat-lavaud.fr>
To: Sean Turner <sean@sn3rd.com>
Cc: TLS List <tls@ietf.org>
Organization: Microsoft Research
In-Reply-To: <D938B161-77F8-4C5A-A407-4E6B7609D02A@sn3rd.com>
References: <D938B161-77F8-4C5A-A407-4E6B7609D02A@sn3rd.com>
Message-ID: <4069dbe044d1b016bf12623b17ac0ec0@delignat-lavaud.fr>
X-Sender: antoine@delignat-lavaud.fr
User-Agent: Roundcube Webmail/1.2.3
Archived-At: <https://mailarchive.ietf.org/arch/msg/tls/6TxyS80c3uel5g1ERV9iDo0ujqk>
Subject: Re: [TLS] Adoption call for draft-rescorla-tls-ctls
X-BeenThere: tls@ietf.org
X-Mailman-Version: 2.1.29
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: Mon, 25 Nov 2019 13:49:52 -0000

I support this effort, and would like to point out that we have recently 
published a paper [1] and a collection of tools [2] to automatically 
verify the security (non malleability) of binary message formats, which 
we successfully applied to all of TLS [3] (which revealed many small 
specification errors in published RFCs, and some malleability problems 
such as the lack of tag in the CertificateEntry type).

Using this collection of tool, if the new compact format is expressible 
in the same syntax as TLS, it may be relatively easy to formally prove 
that the compact and full message formats are equivalent (and most of 
the proof is automated), by writing the lifting from the compact to the 
full specification types. I also recommend to formalize the message 
format specification language such that automatic tools like ours can 
directly operate over the formats described in the RFC.

[1] 
https://www.microsoft.com/en-us/research/uploads/prod/2019/05/20190601everparse.pdf
[2] https://github.com/project-everest/everparse
[3] 
https://github.com/project-everest/mitls-fstar/blob/dev/src/parsers/Parsers.rfc

Best,

Antoine

On 2019-11-21 05:36, Sean Turner wrote:
> At IETF 105, ekr presented cTLS (Compact TLS) [0][1][2] to both the
> TLS WG and the LAKE BOF, which is now a chartered WG [3].  After some
> discussions, the ADs suggested [4] that the TLS WG consider whether
> this draft be adopted as a TLS WG item. LAKE could then later
> specify/refer/adopt/profile it, as appropriate. The authors revised
> cTLS and presented the revised draft at IETF 106 [5].  At IETF 106
> there was support for adoption of cTLS as a WG item.  To confirm this
> on the list: if you believe that the TLS WG should not adopt this as a
> WG item, then please let the chairs know by posting a message to the
> TLS list by 2359 UTC 13 December 2019 (and say why).
> 
> NOTE:
> : If the consensus is that this draft should be adopted as a WG item,
> then this will necessarily result in a WG rechartering discussions.
> We would have gotten to this rechartering discussion anyway now that
> DTLS 1.3 is progressing out of the WG.
> 
> Thanks,
> Chris, Joe, and Sean
> 
> [0] https://datatracker.ietf.org/doc/slides-105-tls-sessa-ctls/
> [1] https://datatracker.ietf.org/doc/draft-rescorla-tls-ctls/
> [2] https://github.com/ekr/draft-rescorla-tls-ctls
> [3] https://datatracker.ietf.org/doc/draft-rescorla-tls-ctls/
> [4] 
> https://mailarchive.ietf.org/arch/msg/lake/kACwW7PXrmTRa4PvXQ0TA34xCvk
> [5]
> https://datatracker.ietf.org/meeting/106/materials/slides-106-tls-compact-tls-13-00.pdf
> _______________________________________________
> TLS mailing list
> TLS@ietf.org
> https://www.ietf.org/mailman/listinfo/tls