Re: [TLS] Fwd: Re: AD review of draft-ietf-tls-dtls-connection-id-07

antoine@delignat-lavaud.fr Sun, 11 October 2020 21:26 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 9E4AB3A08AA; Sun, 11 Oct 2020 14:26:15 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.099
X-Spam-Level:
X-Spam-Status: No, score=-2.099 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, URIBL_BLOCKED=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 hZP_08Rftt3j; Sun, 11 Oct 2020 14:26:12 -0700 (PDT)
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 498753A08D3; Sun, 11 Oct 2020 14:26:11 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=delignat-lavaud.fr; s=dkim; h=Content-Transfer-Encoding:Content-Type: MIME-Version:Message-ID:Date:Subject:In-Reply-To:References:Cc:To:From; bh=nxx39BdCAp7sGpFb0hXtL/ktNsXR6lsZz6Z2XXbFhuo=; b=n+WiBpbamHz5F2t+hNvJtHs8f5 1Fp7w+icssttjokQkmzwVpntvWQeHc5Iv5TzAWmz2gOe+l7bc1CqNyFcjT+Djl2lKSyprZXS4bZXS tYtgSk0HLEeTkrPWtmnBSzh5vS8ERreMKfg8VMVVwfjWtUAwUBlfvADYoL7S6NxMlUwBRTeSPe+Ce hgs78lBpC4f9WTH/G8h2ayqES15HzWnl5kpPpEmZLt7kXuskk7W9rB7YuOBHRKJwOBGgC7Ty0P5VU SH0vZZgeXpjdLTZqZfF6dq/Dv0lx+LgdReVmKF8h2w30ECRD+y3a7TfdalDDqYmWTCK3mkd5SIi39 Itf7hFmA==;
Received: from localhost (authenticated.user.IP.removed [::1]) by argon.maxg.info with esmtpsa (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (envelope-from <antoine@delignat-lavaud.fr>) id 1kRir2-0002bB-Fo ; Sun, 11 Oct 2020 23:26:08 +0200
From: antoine@delignat-lavaud.fr
To: 'Watson Ladd' <watsonbladd@gmail.com>, 'Achim Kraus' <achimkraus@gmx.net>, taramana@microsoft.com
Cc: draft-ietf-tls-dtls-connection-id@ietf.org, tls@ietf.org, 'Benjamin Kaduk' <kaduk@mit.edu>
References: <0da9b525-ec78-bef5-6ceb-5f377019ade4@gmx.net> <4ca7c2f9-1e9d-0d16-0089-649f013b4565@gmx.net> <20201008233454.GF89563@kduck.mit.edu> <6185242d-8ba8-2d2f-5938-afad46c2e854@gmx.net> <20201009212240.GK89563@kduck.mit.edu> <fe7eab66-a14a-5f18-46be-7bae471c3b20@gmx.net> <CAOgPGoBWRyqQUNk3JQx2_Cna-7s-A7gENVwW-sh8+tRoJ_=V_Q@mail.gmail.com> <13a821d3-30cc-94b8-842c-22a87d280f09@gmx.net> <CACsn0cn4QcnaoocQeoiUXgGoAvfOs+1+Ei76z1Kuq8MMqNEh3Q@mail.gmail.com>
In-Reply-To:
Date: Sun, 11 Oct 2020 23:26:03 +0200
Message-ID: <2cec01d6a015$23280130$69780390$@delignat-lavaud.fr>
MIME-Version: 1.0
Content-Type: text/plain; charset="utf-8"
Content-Transfer-Encoding: quoted-printable
X-Mailer: Microsoft Outlook 16.0
Content-Language: fr
Thread-Index: AQG8OCdvRyMzN6gdfhDRUC0fSvvW1wJeYsnhAhccQ0QCpR/r1gGzgLtVAbk0pCoB2tYMpAKgELGdAlQjCkAB6PTzb6ktuFhQ
X-Invalid-HELO: HELO is no FQDN (contains no dot) (See RFC2821 4.1.1.1)
Archived-At: <https://mailarchive.ietf.org/arch/msg/tls/f7_mHj-y0rijJHb0szvNjWdZ53c>
Subject: Re: [TLS] Fwd: Re: AD review of draft-ietf-tls-dtls-connection-id-07
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: Sun, 11 Oct 2020 21:26:16 -0000

P.S. additional comments for the authors of the cTLS draft:

- it is absolutely not acceptable to tolerate two different finish values for the same handshake depending on which codec was used to carry the handshake messages. This would be an attack against the security definition of TLS in virtually every model that was published, symbolic or computational.
- it is actually very easy to prove the security of cTLS modularly (i.e. without changing anything in the security model of normal TLS). The idea is to express cTLS as an injective type cast, as suggested by others in the thread.
The argument for the security is based on the parser synthetizer combinator, which takes a parser p for type t1 and an injective function f:t1->t2 and returns a parser p' for the type p2. It is possible to generically prove that the combinator preserves the strong prefix property. See https://github.com/project-everest/everparse/blob/master/src/lowparse/LowParse.Spec.Combinators.fsti#L487 (and corresponding fst) for the proof.
Writing and proving the injectivity of the f function is probably quite easy, as it's a function defined a high-level representations (and it's mostly filling missing fields with default values). We don't have time to do it now but if someone wants to get familiar with F* and the EverParse framework it's probably achievable to a beginner with some experience in program verification and functional languages.
- the generic argument only works if both peers know in advance which codec they want to use. If some clients and servers may accept both, something must be done to ensure that the same codec was used by both peers if the security model expects they must use the same codec (unless it is an explicit goal to allow an active adversary/"middleboxes" to re-encode transparently to the peers). 
An easy way to do this is to see the codec as a transport layer negotiated parameter which is authenticated in the handshake with an added extension (similar idea to QUIC TP).
If the CH is shared by both codecs it is possible to negotiate cTLS with a normal extension.

Best,
Antoine

-----Original Message-----
From: antoine@delignat-lavaud.fr <antoine@delignat-lavaud.fr> 
Sent: dimanche 11 octobre 2020 22:54
To: 'Watson Ladd' <watsonbladd@gmail.com>; 'Achim Kraus' <achimkraus@gmx.net>
Cc: 'draft-ietf-tls-dtls-connection-id@ietf.org' <draft-ietf-tls-dtls-connection-id@ietf.org>; 'tls@ietf.org' <tls@ietf.org>; 'Benjamin Kaduk' <kaduk@mit.edu>
Subject: RE: [TLS] Fwd: Re: AD review of draft-ietf-tls-dtls-connection-id-07

Dear Watson,

I object to your comment about formal models of TLS not capturing wire encoding issues. miTLS does in fact formally specify the format of all messages on the wire to the bit.
In fact this is complex enough that we have a full paper just about the subject that will tell you more or less everything that was said in this thread http://antoine.delignat-lavaud.fr/doc/usenix19.pdf - https://github.com/project-everest/mitls-fstar/blob/dev/src/parsers/Parsers.rfc is the formal TLS message format specification including the demonstrably unsafe constructions (implicit tags on server key exchange in 1.2 and CertificateEntry in TLS 1.3). 

In the specific context of connection ID, QUIC up to draft 16 did suffer from an attack caused by the lack of encoding of the CID length. The attack is caused by the concatenation of two variable length fields in the network format (the CID and the packet number) that can both be tampered by an active attacker. The boundary of the concatenation is made ambiguous to the crypto authentication (AAD of packet content encryption) by QUIC header protection, which is applied before decryption. See https://eprint.iacr.org/2020/114.pdf (Section III.D) for a description of the attack. See https://github.com/project-everest/everquic-crypto/blob/master/src/QUIC.Spec.VarInt.fsti and https://github.com/project-everest/everquic-crypto/blob/master/src/QUIC.Spec.VarInt.fst  for the formal proof that the QUIC varint encoding with minimal length representation satisfies the strong prefix property.

Antoine

-----Original Message-----
From: TLS <tls-bounces@ietf.org> On Behalf Of Watson Ladd
Sent: dimanche 11 octobre 2020 08:50
To: Achim Kraus <achimkraus@gmx.net>
Cc: draft-ietf-tls-dtls-connection-id@ietf.org; tls@ietf.org; Benjamin Kaduk <kaduk@mit.edu>
Subject: Re: [TLS] Fwd: Re: AD review of draft-ietf-tls-dtls-connection-id-07

On Sat, Oct 10, 2020 at 11:27 PM Achim Kraus <achimkraus@gmx.net> wrote:
>
> Hi Joe,
>
>  > [Joe]  It's unfortunate to find issues that require breaking change 
> at  > the end of the review cycle, especially for a draft that has taken a
>  > long path to get here.   If there is an issue that is exploitable, even
>  > in a corner case, someone will develop an attack, clever name, logo and
>  > website and we will all have to scramble to deploy a fix.   It's better
>  > to fix now rather than later.
>
> Agreed, therefore I wrote at the begin of the discussion with Ben:
>
>  >> I would prefer, if this is not changed again without strong  >> 
> arguments!
>
>  > In this case, I don't have a way to  > exploit this issue, but 
> unless someone has a way to demonstrate that  > this is not going to 
> be an issue then I believe it is prudent to fix it  > now.
>  >
>
> In my opinion, ONE change may be possible. A server may be configured 
> to use only the old, only the new, or both by "try on the client's finish".
> I'm not happy with such "dirty" work-around. I would prefer to do so 
> for something more the "cryptographic hygiene".
>
> So, if the MAC is considered to be adpated again, should it not be 
> discussed, why at all the cid-length should be put in?
> I asked this already in January 2019
>
> https://github.com/tlswg/dtls-conn-id/pull/29#discussion_r246654915
>
> The MAC contains already a overall length. Even in that discussion, no 
> one mentioned the reason for adding it. So if there a doubts about 
> injection, why not remove it at all?

The doubt is because of where it appears not that it appears. If every value was preceded by its length the encoding would obviously be injective. Here though it isn't clear if two different inputs to the encoding could end up the same. In fact I think in the MAC setting there almost certainly is a problem as the length of the ciphertext is right after the cid length, and with some cleverness you can come up with a cid and ciphertext that could be interpreted multiple ways.
Unfortunately I haven't followed the draft's discussions that closely.

I do not understand how a CID is supposed to be parsed by a recipient when the length can change and the length field is not encoded, but perhaps I'm misreading the intent of the [] notation in the record layer of the draft.

>
>  > Would this issue have been caught by formal verification?
>
> That may also be something to help, not to change still again and again.

I don't think the formal models of TLS reach the wire encoding.


--
Astra mortemque praestare gradatim

_______________________________________________
TLS mailing list
TLS@ietf.org
https://www.ietf.org/mailman/listinfo/tls