IETF Logo Mail Archive

Re: [MLS] Formal proof for PR 713 / "Improve parent hash guarantees"

Raphael Robert <ietf@raphaelrobert.com> Fri, 10 June 2022 10:16 UTC

Return-Path: <ietf@raphaelrobert.com>
X-Original-To: mls@ietfa.amsl.com
Delivered-To: mls@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id ED73AC15AAC4 for <mls@ietfa.amsl.com>; Fri, 10 Jun 2022 03:16:01 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.005
X-Spam-Level:
X-Spam-Status: No, score=-2.005 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, HTML_MESSAGE=0.001, HTTPS_HTTP_MISMATCH=0.1, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, URIBL_BLOCKED=0.001, URIBL_DBL_BLOCKED_OPENDNS=0.001, URIBL_ZEN_BLOCKED_OPENDNS=0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (1024-bit key) header.d=raphaelrobert.com
Received: from mail.ietf.org ([50.223.129.194]) by localhost (ietfa.amsl.com [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id l3RmlAiFGvXn for <mls@ietfa.amsl.com>; Fri, 10 Jun 2022 03:15:57 -0700 (PDT)
Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com [IPv6:2a00:1450:4864:20::433]) (using TLSv1.3 with cipher TLS_AES_128_GCM_SHA256 (128/128 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id BAFC9C15948E for <mls@ietf.org>; Fri, 10 Jun 2022 03:15:57 -0700 (PDT)
Received: by mail-wr1-x433.google.com with SMTP id m24so1026485wrb.10 for <mls@ietf.org>; Fri, 10 Jun 2022 03:15:57 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=raphaelrobert.com; s=rr; h=from:message-id:mime-version:subject:date:in-reply-to:cc:to :references; bh=S/NM+K15HC7hLDStDWCBQvc2PPCQ5G5Agvtv0XdP2Go=; b=fGPd+2AsBJBCnzNpr5URFdZAcHQVb9Y7j8sD8vyZFixVtGY8ANb15T6xcVbH+Sw5KV ljwy2VZaCk9suqxyyZoa+9wZKp2qjuKX8qSWKUzNRh4DV56d+PkZIZX1E31NrB3QxIeO gQhHpxKpRqEe5fAjGtzurKLNgHHHY1uCjI6Ns=
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:from:message-id:mime-version:subject:date :in-reply-to:cc:to:references; bh=S/NM+K15HC7hLDStDWCBQvc2PPCQ5G5Agvtv0XdP2Go=; b=OL9JE64M44i4TbE/kHJ5/Liss25/KJMNk+xqe565rXWX2yYK1JWO9c8gHDfi0r+XQs tnDgXAJJcLLzqnyGV+SdrYXlO8wO0S5KgsVsJf85QcO8aILGiAFcpyhlJrkeygXKi5h3 OJa1MlAL9qTeKKLVvm+An7+03/F+FgmuVuyihmWJ5jctAxLMqPa6JeOP9DefCI8wT+C2 s+K+6B+XZTulIOUOeoiUJd8VU7EGfJeUoynjo3ANscUN81daDzNHOOMHtH76LpPlLWfD 4tZvk6wmCp2GcB8MU1OvDKy8dpgbExAqzidPR+Iv8HbVqmH2cwZU34tizW97YUyDMi7n ZflA==
X-Gm-Message-State: AOAM533YtV5oH0M9YHvlCKwOafE8ogXvxmQ/LtOKOXYJ1PK78T/lHw1X buckm1RxCXPFhFtxqBXqW63N4w==
X-Google-Smtp-Source: ABdhPJz/uELAvX+kdbqYS5jW+8EYol5t+Nrjz6S0L0MVBWI2Zta7oF9RZB6PF/qux2JMXpTbqevqxQ==
X-Received: by 2002:a5d:648b:0:b0:215:da35:3a6b with SMTP id o11-20020a5d648b000000b00215da353a6bmr34226725wri.358.1654856155068; Fri, 10 Jun 2022 03:15:55 -0700 (PDT)
Received: from smtpclient.apple (ip-095-208-241-080.um33.pools.vodafone-ip.de. [95.208.241.80]) by smtp.gmail.com with ESMTPSA id r8-20020adfdc88000000b0021576694d9dsm20396320wrj.97.2022.06.10.03.15.53 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Fri, 10 Jun 2022 03:15:54 -0700 (PDT)
From: Raphael Robert <ietf@raphaelrobert.com>
Message-Id: <31BAF321-0E80-473C-AE15-EA2C11B61E4D@raphaelrobert.com>
Content-Type: multipart/alternative; boundary="Apple-Mail=_6245C41D-EC84-420A-979F-C4BFC6EE3259"
Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.100.31\))
Date: Fri, 10 Jun 2022 12:15:52 +0200
In-Reply-To: <BLAPR09MB68340D279F0E6CDBBA9D77B1EAA69@BLAPR09MB6834.namprd09.prod.outlook.com>
Cc: Richard Barnes <rlb@ipv.sx>, Théophile Wallez <theophile.wallez@inria.fr>, Messaging Layer Security WG <mls@ietf.org>
To: "dbnisbe@uwe.nsa.gov" <dbnisbe=40uwe.nsa.gov@dmarc.ietf.org>
References: <7e5a8152-ef25-7ab4-b265-8e2e27756038@inria.fr> <CAL02cgTT=A7cgK3UKzAGLci+Q2rSixBSAptAdh70+5pdr8-YGA@mail.gmail.com> <BLAPR09MB68340D279F0E6CDBBA9D77B1EAA69@BLAPR09MB6834.namprd09.prod.outlook.com>
X-Mailer: Apple Mail (2.3696.100.31)
Archived-At: <https://mailarchive.ietf.org/arch/msg/mls/Hu0z1dU1avLCM-eHjEs-I0eszmU>
Subject: Re: [MLS] Formal proof for PR 713 / "Improve parent hash guarantees"
X-BeenThere: mls@ietf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Messaging Layer Security <mls.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/mls>, <mailto:mls-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/mls/>
List-Post: <mailto:mls@ietf.org>
List-Help: <mailto:mls-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/mls>, <mailto:mls-request@ietf.org?subject=subscribe>
X-List-Received-Date: Fri, 10 Jun 2022 10:16:02 -0000

FYI we held the meeting yesterday before the interim.

Raphael

> On 10. Jun 2022, at 09:23, dbnisbe@uwe.nsa.gov <dbnisbe=40uwe.nsa.gov@dmarc.ietf.org> wrote:
> 
> I’d like to join. Thank you!
>  
> -Daphanie N.
>  
> From: MLS <mls-bounces@ietf.org> On Behalf Of Richard Barnes
> Sent: Wednesday, June 8, 2022 9:21 AM
> To: Théophile Wallez <theophile.wallez@inria.fr>
> Cc: Messaging Layer Security WG <mls@ietf.org>
> Subject: Re: [MLS] Formal proof for PR 713 / "Improve parent hash guarantees"
>  
> I've got a calendar invite going with Webex coords.  Let me know if you'd like to join.
> --RLB
>  
> On Wed, Jun 8, 2022 at 4:14 AM Théophile Wallez <theophile.wallez@inria.fr <mailto:theophile.wallez@inria.fr>> wrote:
> Hello All,
> 
> During the last interim, when discussing PR 713, people raised concerns 
> that this PR might introduce bugs in MLS, because the parent-hash is a 
> complex thing and contained many bugs in the past.
> 
> During the last days, I formalized a small part of MLS in F*, and proved 
> that the invariants checked in the "Verifying Parent Hashes" section are 
> actually invariants of the protocol.
> 
> Of course I can't just say "believe my I have a formal proof". I also 
> can't just send my model as-is and expect everyone to decipher the F* 
> code without explanations.
> Richard therefore proposed to meet during one hour before the next 
> interim, for the people interested, during which I will explain my 
> model, hoping that afterwards:
> - you will agree that my code faithfully models the parts of MLS dealing 
> with parent-hashes,
> - you will agree that the theorem I proved actually state that the new 
> invariants are preserved.
> The only prerequisite will be to be a bit familiar with functional 
> programming (no need to know super fancy stuff, just algebraic datatypes 
> / pattern matching / recursion should be enough).
> 
> Richard will take care of setting up a Webex link.
> 
> Cheers,
> Théophile.
> 
> _______________________________________________
> MLS mailing list
> MLS@ietf.org <mailto:MLS@ietf.org>
> https://www.ietf.org/mailman/listinfo/mls <https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.ietf.org%2Fmailman%2Flistinfo%2Fmls&data=05%7C01%7Cdbnisbe%40uwe.nsa.gov%7Cd26f5aec74f940bc07ab08da4951d349%7Cd61e9a6ffc164f848a3e6eeff33e136b%7C0%7C0%7C637902913052116953%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=1K10VHuq3P5Y2Ro1V1XM%2BHn881Ev3Ew%2BTeAmXWWFnSI%3D&reserved=0>_______________________________________________
> MLS mailing list
> MLS@ietf.org
> https://www.ietf.org/mailman/listinfo/mls

v2.23.0 | Report a Bug | By Email