IETF Logo Mail Archive

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

"dbnisbe@uwe.nsa.gov" <dbnisbe@uwe.nsa.gov> Fri, 10 June 2022 07:23 UTC

Return-Path: <dbnisbe@uwe.nsa.gov>
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 5734CC1674FF for <mls@ietfa.amsl.com>; Fri, 10 Jun 2022 00:23:12 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -3.328
X-Spam-Level:
X-Spam-Status: No, score=-3.328 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIMWL_WL_HIGH=-0.745, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, FROM_GOV_DKIM_AU=-0.677, HTML_MESSAGE=0.001, HTTPS_HTTP_MISMATCH=0.1, RCVD_IN_ZEN_BLOCKED_OPENDNS=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 (2048-bit key) header.d=uwe.nsa.gov
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 ov0VLtJycLZT for <mls@ietfa.amsl.com>; Fri, 10 Jun 2022 00:23:08 -0700 (PDT)
Received: from GCC02-DM3-obe.outbound.protection.outlook.com (mail-dm3gcc02on20621.outbound.protection.outlook.com [IPv6:2a01:111:f400:7d04::621]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 729FEC157B4B for <mls@ietf.org>; Fri, 10 Jun 2022 00:23:07 -0700 (PDT)
ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=HpffNjB9K9x4DIIEThoqEk7JteuqdxhQrGpidZEvhqsdFETDs0j7hp12IAFZKPjFBhCT9uy7HKXVrU6DXoR/RMZo42W0YD1oBigqE7NswAb5jC3tjv07DQaw9lb2WspC57aJEQmz674eMpT7iosDQWT2ZwAUiVslVSAbojXwV7K6B6UnvLXEUb8MdrCKECK4gE97vHYxgyjPFmFzKyhDOrKS2n8YDZLe6W7jpvkVjA3TCdKaxfcUbal8sjRAWOTfMXe13hdnqikl+L/MeQUW26IqOPynZbR/+piJIJoSwodNj6OhFbUlr2+mKYWV6uKezhlmgF0xpk6JXucPZgWU8A==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=xEaXgvdnr10gzGbHtksrSumvL0YYbZId4VW2LrhNWyo=; b=YE21flHVp/mgr5gAT+9FhGTLCEvRd7pjQl4+ShcdrP3WJW7tYBX76jlS+Pyd93QhmJOZWXQDniY6nxEqYr5QmzTgzc4wwxHK04lws6xFJdyOp79K8P5YsTwqniADko1ngOtIDQX9nCxeIjr3ON0X4rCHyE8gO5KmVz6NxAj9NaDWYZLgiIo7W/dESOFcsq3Pmg07nLouCiEF1qqtPy+ADEenECF20rJYnyAQvYWpCwqBjUdRZk5z+7gx1qnmo0AxKwlB0DiNLThH/TuMhr/lJj/LOJvkOHQYexoJIIzNOi7tDeCIjrJ8f6rjCsndrfrR4qSUY+GjSVoawB5+0eHslg==
ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uwe.nsa.gov; dmarc=pass action=none header.from=uwe.nsa.gov; dkim=pass header.d=uwe.nsa.gov; arc=none
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=uwe.nsa.gov; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=xEaXgvdnr10gzGbHtksrSumvL0YYbZId4VW2LrhNWyo=; b=IRz9DHmnStAHcJKrcDdKzsIcBvR8ETFbXM7IIcMk9Bz/HMAmwRkMcVQ35N+0e/XgD09TzJp/nlDauZHqASzMWiJL2rRB0gIE8bDXrgY9mLpcrJrWgBAAv1w/wMqUfGo8JwoxaHedmP7rPln7A1YZ+hYFmcabk55ZQ5q4BnM+FtmhXQfW/ePe6oUN6Kg6YarcYulxfhR+2ZFnLmyzGSfXeXLNW3GkhM1b/TyHwKZjPvNgBMVyjC1kW6ETWHyPAWZE8q1rTqFBDOQTIerhfawZgoMSK23EWffKbVcauohq+dbrjmOZcVU3GSQWzc6JzAJ1n/ItYNGPugCFPxOIYtB55A==
Received: from BLAPR09MB6834.namprd09.prod.outlook.com (2603:10b6:208:288::14) by PH0PR09MB7722.namprd09.prod.outlook.com (2603:10b6:510:68::18) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.5332.13; Fri, 10 Jun 2022 07:23:00 +0000
Received: from BLAPR09MB6834.namprd09.prod.outlook.com ([fe80::7430:ff01:c0c:e57a]) by BLAPR09MB6834.namprd09.prod.outlook.com ([fe80::7430:ff01:c0c:e57a%7]) with mapi id 15.20.5332.013; Fri, 10 Jun 2022 07:23:00 +0000
From: "dbnisbe@uwe.nsa.gov" <dbnisbe@uwe.nsa.gov>
To: Richard Barnes <rlb@ipv.sx>, Théophile Wallez <theophile.wallez@inria.fr>
CC: Messaging Layer Security WG <mls@ietf.org>
Thread-Topic: [MLS] Formal proof for PR 713 / "Improve parent hash guarantees"
Thread-Index: AQHYew/TaG04tQgYj0+JQQ9VLfhMoK1FfyEAgALAZCA=
Date: Fri, 10 Jun 2022 07:23:00 +0000
Message-ID: <BLAPR09MB68340D279F0E6CDBBA9D77B1EAA69@BLAPR09MB6834.namprd09.prod.outlook.com>
References: <7e5a8152-ef25-7ab4-b265-8e2e27756038@inria.fr> <CAL02cgTT=A7cgK3UKzAGLci+Q2rSixBSAptAdh70+5pdr8-YGA@mail.gmail.com>
In-Reply-To: <CAL02cgTT=A7cgK3UKzAGLci+Q2rSixBSAptAdh70+5pdr8-YGA@mail.gmail.com>
Accept-Language: en-US
Content-Language: en-US
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
authentication-results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=uwe.nsa.gov;
x-ms-publictraffictype: Email
x-ms-office365-filtering-correlation-id: 253c9077-f9fc-4851-d081-08da4ab20c97
x-ms-traffictypediagnostic: PH0PR09MB7722:EE_
x-microsoft-antispam-prvs: <PH0PR09MB772298A1AD20477D3C581FE6EAA69@PH0PR09MB7722.namprd09.prod.outlook.com>
x-ms-exchange-senderadcheck: 1
x-ms-exchange-antispam-relay: 0
x-microsoft-antispam: BCL:0;
x-microsoft-antispam-message-info: 2SS9WnrLBQ0aPosqthTrH7W3oL5PRSKtm3485hgnNopNVIQpVaBiZlsvvgUZL9qnBlXQFAOM3SEmMl31YhsI9N/N4PwsUPD/U/RvG8Q6wkQEzIBRTSVOxKJ8+ezbaR2in3E+38sKYOBFbRIlhWeZXAd2hegTIE6l1VPvAuhb+z5JKFiSnENHq4+vMPGyulhfYYL9WMxHzeLqTlcqS9KjR8Zlt51/C0pu9GJCBH1o520BsfAOKPcXbGeKmnkK4TYRfjaYwLYolZOiTZ3NVaarovylguA2WBldRkAMoPV76vTsIWPM2jlXA60Pug4SThZjoVs29dvJ6x1RAjCVBvvoIr/6JTHdWJxzocDFvzKpa8lj9WhKT96bXFmB+StkQWKSz+Y9QnbTEl+HJsR0FLc0gp54ZruLupjceIwq/7iN78f1x0FPpzhrMqmw31FPpxCENskpXOIfuVjhw6whpbVBSTZvgIqvaQJzcuTEVyOIgDnrnj2mQYAd74vW/phIykMMWll1AH5Q2bcvuVTEbCZRJhZvnKuRN5I6TCsZzrQE9TFcuzOAl+lzdEZtVomqq98LNnwLy852v8f2xMoNmwGOkUqJ+xl7ntdNG0/rNPCJz0unI8Ia3YtgV0EW8arY1NvezHahV0mOgKqKfoYEFjqcKXylXXNyBi+yF5uFuWa+haxdnJ0zsIUY2I30e9U+diwhkzKvg50ntFRIsL+1MewxcWTohCJXp7ppQw5Ipq4qSJXWpJGt9tPOkf610VEUYxUi9ST+9J1m0vs1FMzk8fnlFU7kZj5raVG0d/GVBbcRgcc=
x-forefront-antispam-report: CIP:255.255.255.255; CTRY:; LANG:en; SCL:1; SRV:; IPV:NLI; SFV:NSPM; H:BLAPR09MB6834.namprd09.prod.outlook.com; PTR:; CAT:NONE; SFS:(13230001)(4636009)(366004)(110136005)(5660300002)(53546011)(316002)(76116006)(55016003)(82960400001)(71200400001)(7696005)(6506007)(8676002)(4326008)(66946007)(66446008)(64756008)(66556008)(66476007)(122000001)(9686003)(26005)(86362001)(508600001)(83380400001)(966005)(33656002)(186003)(2906002)(52536014)(166002)(8936002)(38100700002)(38070700005)(66574015); DIR:OUT; SFP:1101;
x-ms-exchange-antispam-messagedata-chunkcount: 1
x-ms-exchange-antispam-messagedata-0: Qhom5gzfWYmZCV16yJKbW5ffVVRQHDwaS4C24DkPErQN397xAPeKOPn8ewwMOeE9MKHKRMOzl10vmfZ9yeb5Sq/M4l1iXWHG3owE2glH3P2MW8YDFB0EeJ0SWPBt5p+FuDkSgD6nd7xPVw0eKhp+1djHhyISbs8aA2QsmMnOlAEpf7Qwfph+alg6mKYkERuNXzU9epiV1c714IuwmWQVKYbrScOmPYgLjCLvuMw1gpSco2MCSvsG8QOQtjavhbznHxyQl7QlZKD2T25cPbhvBdmZtik8/fjVyiUFJ6yf2VJtevnQkPaFGBk7wIThz3GYgAYeHu21Ex6KoP0m8G3tS4Bpkcj0/75ufXfQG+Nb5VKZD9FizP/x/WyS17BpZbfaTQtkXiM5JPPuEOVtHidaX8HVEGy+ECqBlkvZr/Yk5B4emJHu8XeitJEHpwD5hm0ZlAz0Dx5Cb1wk43d6u2tTy2ZYD1Zi4bc/QzTV7R8/fo37V1kPjONuyAriObthqAfBuT6kIsLE9HW+zQT3JnYGR01U/PHNM42Yl8AtQx1WvIr2Vr8Ca1KLpG8eIFCIcykC0L2cQh7UZYdymt0aI+jDWnDKkcq1vmeER1aunBMHMkmWmoAEgHnTF8Z+jRYyU4ItnDW1+jJlRk5KKjKyikn24uEDZSiEMD4zduFlfbY6LgBu3CstOGQYqlnQ3RyW+9PUgSMFMM3eXBJqEZdF4p/m+fBV8GTjXH+2eXAxnwYZ7X5OFZsICbDLjuwkDooyKjZEBCeHBi+worXg+G8bSK2XJIP0QcLYuFonLzH3mkx8aMV3OIl2f5p+JH/D30FXajXLt9wCFGhBoOk3KX5NY6PKlPr2wG/kuPWIRYYMo9CQpUQF51dXCURhE5njY3kOnJWoYpliRbCxGGDZoEPClJqtIBwAlPGj6xQnYVQsGoXyt+RuK3vg1ysBRTTfIiZZPM7hC0hfEhzUk0jdIxQhPz37JP4Pn91buOUZojhgbYCfllzENUm2G7dBS/Mspf4QJIg4T8B0HLu6qMCi0/i6x+6KeMFkEmCH+o+cRboQ4t8ohIu5Jw0sF6sQRoVW7SLRFUIYwuRcnu3TvTxyA4dRqOZZjxIWwgjlL6P8y+qsBMme1ixTY8ytGkMbFZx7cjcT6tomy8mM3PxwekTU0jfFm4H4XqwL4hTZ9/cd9iYnIqS7v5C/lViPw2VT0P1ZubHMhgVdHK4DEtSrtxPwPs7A3LNt2WorKbq7t53ePZcFlKzF8HnDRkWZtMP6rO7hgHjLuWXip3PnPX9LtN7eyTGClyX5YROwns29qbg8gcjaQf+MhzEaljlw4lK4JUfcZyufJb68KFfffZRWzpDjj/qo10WSk6VHhnsV5LQ3gAF0KhdQVYZQDi1V5qBCVeAJJi+8F33z63G6IFXkLyMEwhz1ofvgbCNPgw47VW3GHcRC7XtW1a7W7GHvbnOdIZYPnjskSsQTuecbA1xwsesCCJhSxMeQ6ECUaDAtQBymSV85rN41ffZdLzYZoNNjY+ewXxLtMbAO2Ss4eZYOOxL44tHXTuzeUqhJy0PfyhOV6cMRUl7F6uOPVzZhDGjcrjoY5CVreeF20U8MmIRMir2MKJ/RqwCNoXlSHM3hyMjH/lFCJ5QBqyTL4fJGOCjwKpO5bjeUt/Yw8koKiwBCo8vzW1dGOdbXO07YnSKZdIcZSAJpQiffTIhD8Mkmikqz1ZxMesupfR/Jk/1v0++sbGQQtpVE7eI+iQ==
Content-Type: multipart/alternative; boundary="_000_BLAPR09MB68340D279F0E6CDBBA9D77B1EAA69BLAPR09MB6834namp_"
MIME-Version: 1.0
X-OriginatorOrg: uwe.nsa.gov
X-MS-Exchange-CrossTenant-AuthAs: Internal
X-MS-Exchange-CrossTenant-AuthSource: BLAPR09MB6834.namprd09.prod.outlook.com
X-MS-Exchange-CrossTenant-Network-Message-Id: 253c9077-f9fc-4851-d081-08da4ab20c97
X-MS-Exchange-CrossTenant-originalarrivaltime: 10 Jun 2022 07:23:00.1631 (UTC)
X-MS-Exchange-CrossTenant-fromentityheader: Hosted
X-MS-Exchange-CrossTenant-id: d61e9a6f-fc16-4f84-8a3e-6eeff33e136b
X-MS-Exchange-Transport-CrossTenantHeadersStamped: PH0PR09MB7722
Archived-At: <https://mailarchive.ietf.org/arch/msg/mls/qg0lS_LbrDSFL8BhX9cyUpYCNjQ>
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 07:23:12 -0000

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>

v2.23.0 | Report a Bug | By Email