IETF Logo Mail Archive

[CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and Tamarin Symbolic Protocol Analyzers

Peter Gutmann <pgut001@cs.auckland.ac.nz> Tue, 03 November 2026 05:40 UTC

Received: from SY8PR01CU002.outbound.protection.outlook.com (mail-australiaeastazlp170100001.outbound.protection.outlook.com [IPv6:2a01:111:f403:c40d::1]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange secp256r1 server-signature ECDSA (prime256v1) server-digest SHA256) (No client certificate requested) by mx.ietf.org (Postfix) with ESMTPS id 70AB64B for <cfrg@ietf.org>; Tue, 03 Nov 2026 05:40:47 +0000 (UTC)
Authentication-Results: mx.ietf.org; dkim=pass header.d=cs.auckland.ac.nz header.s=selector1 header.b=Td9xovm5; spf=pass (mx.ietf.org: domain of pgut001@cs.auckland.ac.nz designates 2a01:111:f403:c40d::1 as permitted sender) smtp.mailfrom=pgut001@cs.auckland.ac.nz; dmarc=pass (policy=reject) header.from=cs.auckland.ac.nz; arc=pass ("microsoft.com:s=arcselector10001:i=1")
ARC-Seal: i=1; a=rsa-sha256; s=arcselector10001; d=microsoft.com; cv=none; b=L5CjFwNljhtc7hC2bfqb8aTvepbvTQEZ4d4fAnrWXEPSwDoZtmK3VIll4V2hIAzNJbWY54cDzYqPUJH0ZCaQ340jVwTPxJ8G3FQGa0R4ZLgdXW6ZZUlYOIDi3kPKri0lJJRay9OuyES7ar9PViUT801RM0QujUxiyUTpy88Ff55vPYZj+dhwdPGnOqlVDPt1HV7Hae3xoQv+lEgy14+tqfScYTdVDQEetrqrY//wjoouldzhlPWC51bkQPjI0Rdy2XNzy8yqgRub6yzGlSK3e6cyOhhsYDCvL4eudBBIPcxGzwm8YObK0Rf4DkfL/DTLybmWzULnPxuoacxhCkqOdw==
ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector10001; 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=TS8S4+OQxd4QhQDs5NjRUDrYtRvKfB55gMvw85827x0=; b=IbhPRfNdopwwJSFzEFXSv/72qKCI1TY9/JJGticroSdQtww/lb21wgxqwdbwkfpTVTiTWh991XhXCR6swdDhDDHSkzVwo1x9szWfik6gTzjMCmg/0DPuTSNNDQKifbIBEprJdy9nCScLTfdjdv4dh1lfMr2+2lDDYaStcarXah+d4W0FTMQ2CBdMTXRrmMx8IAnt+u3Y73j4Nd6MzElbr0hQgTEgVK22VmO1LGEXAauXih4pSgqx2LjTMNcgsey0CqgO1iqnzCtXFSS1kPkdhQYqaz24iKQ5LVvSg6dLitwHV2vZu5QuRJQIIkUJlCOWlwWNehkz8SaKdknE5jA50w==
ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=cs.auckland.ac.nz; dmarc=pass action=none header.from=cs.auckland.ac.nz; dkim=pass header.d=cs.auckland.ac.nz; arc=none
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=cs.auckland.ac.nz; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=TS8S4+OQxd4QhQDs5NjRUDrYtRvKfB55gMvw85827x0=; b=Td9xovm596rq26qHzI8tHZff4wwF1XDoRNr+h6csSHHmmoyOG+1sHHT5Rkc6YuWN3J2DvV0BF857kn+6xdTbgUkJQG2Xr1+Lvnc0RGWs7ORKdQsQ+XtAk9Zl9neQe/ZxIK6TNRk/Bn6wXeDxmXwNyplqd44w2shyKar4eg+Z06uonD7wLW95F6he6cBENpDqqtwaPtFXZByCwOdIq7X+9Ts7FxTTmn+Vv/IIMlRzX33Bdiv94hrcdAEcTtOGSLFcKT+MBYYnsUfB+a9wVAga3oUKaYa0afsVfjHFQzSBeZpuqTaNAGe4czhq3hMqre79rrsa9IzppuGB+hsgEdKYjA==
Received: from SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM (2603:10c6:10:37d::12) by ME0P300MB0445.AUSP300.PROD.OUTLOOK.COM (2603:10c6:220:229::19) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.21.569.12; Tue, 3 Nov 2026 05:40:35 +0000
Received: from SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM ([fe80::7479:9a09:99c7:463d]) by SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM ([fe80::7479:9a09:99c7:463d%7]) with mapi id 15.21.0569.011; Tue, 3 Nov 2026 05:40:33 +0000
From: Peter Gutmann <pgut001@cs.auckland.ac.nz>
To: Ilari Liusvaara <ilariliusvaara@welho.com>, "cfrg@ietf.org" <cfrg@ietf.org>
Thread-Topic: [CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and Tamarin Symbolic Protocol Analyzers
Thread-Index: AQHdauGNUHCIW4VguESjYfuUK5qgSLcbGpAAgAC7HuY=
Date: Tue, 03 Nov 2026 05:40:33 +0000
Message-ID: <SY9P300MB88147744AD3B9D6899E5D94322EE692@SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM>
References: <1A7A2227-C395-44C4-8FF3-6A70EAB70038@symbolic.software> <CAMm+LwjZLpe3G2D6xeoT6bx9h7xJdqbozgHep9-ky3qmcHOOyw@mail.gmail.com> <aujWpqL6w4eQVj_U@LK-Perkele-VII2.locald>
In-Reply-To: <aujWpqL6w4eQVj_U@LK-Perkele-VII2.locald>
Accept-Language: en-NZ, en-US
Content-Language: en-NZ
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
msip_labels: MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_Enabled=True;MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_SiteId=d1b36e95-0d50-42e9-958f-b63fa906beaa;MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_SetDate=2026-11-03T05:40:33.014Z;MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_Name=Internal;MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_ContentBits=1;MSIP_Label_b75eb9d1-7479-4f8a-9240-cc5b19dbbc64_Method=Standard;
x-ms-publictraffictype: Email
x-ms-traffictypediagnostic: SY9P300MB881477:EE_|ME0P300MB0445:EE_
x-ms-office365-filtering-correlation-id: a31eb61a-bf23-47a6-3a31-08df396cfaf6
x-ms-exchange-senderadcheck: 1
x-ms-exchange-antispam-relay: 0
x-microsoft-antispam: BCL:0;ARA:13230040|786006|366016|1800799024|23010399003|10070799003|376014|38070700021|261021123027099003|5023799004|11063799006|4143699003|56012099006|261009223027099003|261028144727099003|261026121527099003|261021121427099003|261026140227099003|261022105027099003|10067099003|18002099003|22082099003|261102123227099003|3023799007;
x-microsoft-antispam-message-info: RgJZrbhO6NLZMNCT4kIzxMADTSwZWeqr5me1zJwaTmHNcQggL9wvdn9GabQXAup/O9u87UmCXXiIo8TMNZL9AG613WsKAm3g+qDC2YCarp+3H5HUPjDYzWJUgvH+wJ8B0HwkkILrxehN+9n8vGHxTMzsSs8cbvMe3Bpvj99cAwJQ7WtTrrmPyAMqXXjZpeutebWWfGOBqvvaxcm6Gs3bBQSsg0GtkXcW6Cy7oWtsUj1QkEQi8FbJzzL0oHvIa8QDIQoMcX+Ee4cQzF+ve0hTgWeFNO6d1eeadzEJtVEGRDNuX+oFPUjJ/2qj3I89okC61NKexCKCpw2m8DEiVLsY5Sa8eckzpAdkJONXc5GyGSrMs8L6PZh/F/mAY7CVhTcMXS9pB0SU9jxXMnRft7TNpqMJC6g55QeyPpl0SkNWDBJvjcRGYs/I/eVmavKN2kC2uhlqsNlb8WUUorezvb9Y3O9c51DqDwUKyZ1e0hVXNsICSigRgkt26hVWlGf4vomOeuV04PfW6tjcGWe940weHFB5w2yoh//LOABDGqQqUSqbJ2ftD2yaxS8pt2faF6XA8Q9EmiAdNd8XZGE3ENGJ/ZDON1RLHBky2vfWRX8E5ezJOYgcQD7j44UtsMSH+d1mHbjH4ukTZKIuAO3WsQ1UPPmQVTMyNOP3oiqNHCgcpcS5CaHdACMfPYtHXgEO10+R+rbRB9dBa074sA6Jz0EWbQ==
x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(13230040)(786006)(366016)(1800799024)(23010399003)(10070799003)(376014)(38070700021)(261021123027099003)(5023799004)(11063799006)(4143699003)(56012099006)(261009223027099003)(261028144727099003)(261026121527099003)(261021121427099003)(261026140227099003)(261022105027099003)(10067099003)(18002099003)(22082099003)(261102123227099003)(3023799007);DIR:OUT;SFP:1102;
x-ms-exchange-antispam-messagedata-chunkcount: 2
x-ms-exchange-antispam-messagedata-0: Hz+bfOlfHAfFS71NkPV515l20EWKly9LWkHAGeNHg/6ED7wkDRQWEBzwtDO9mHG82PnO93Z+y1es+R++i34Kztu3aMrkPWerqp3098EDWahrKMUOEuRRBX/tgx9ljrEDjhqauOO8g09a8JsMAyhDP+yLUXxaz0QQy+fqhqgiIKZYwS/4VgSvfrMLxIpkRdSriwpNPskrYZU8yDXzjxMsu64nkDGp0a6jG5Jj6bXLLHptp+1Aun7VWQ325sl7QDpOlKTdf3ZD77T25pVe8eFf4wEp5yP+xvzS2luDO9O885LeEH21IGCPclMGmSleDdYwDnE9VeynWs0RigXTc9AwslCFijsggShIjm1bfCKeSXnQ6+ZP6LUqtYDh4mCozLC0rLSKwMjC6++BO3kqwp/Ob+8cjJEmoVlPcvZ5X6tLVVeeApFg3i8EdRMxS2gjI3+ToA3bY/EbLnQvF4ZEC2b7HiYL5z8glEk3nm1nvSBk6mFI/Zw7dTpm5yU9XQd9s/rmUBXKAkQsl3V+dD0acexnmQdVvmjjgt2HOkf86uTy6V0XtVKHzxY56gLi6sz/btIiGBxVx2zntd2JW9QYog4afY6FX1A2HmO+68QDnV2eVlqd7bWXyD2c46IYK7bBB4Ii85Push9+2z0DQe+IG5s9EP3jSM+iVbnJgyC+54fTyv5w+0utCWozHzRS5agM3Emc9iEkXS4o8liinRb0jh2Wy70XTYVE/ni5A0WApGZwR8+ty6EmF/INXLhHXYyFIz4WLpmmKWNoLJS6XmT4vJB++EMmSIVU3H1ZnZTOaS5Fgda3/0godIyCetkIqIcp9vCxX7ugvJLo2r2cMqDoTIic08wZ5jagzoFIre7ltLJGTvDRM8Vovp+BOSGxBHovi3FHcax9RinnchFalbftCweW7LtknMZehXCH0eLjY+v1oPhB7ZqENvISRzJI84DvO83fOlL/NGMKffAtWFKpMrCZ8UUre2SyC4WuPUC+FW+3ViPlFHbJseSTKwrp0+yYIVnpPARrHYoZwYBPmxs9vZcWaErPOS34PM4+udFsph2M75H5vipMOMStyfXWFT2zT6upLD3orQ9lw8ZoxKA4i6jb6YUrwQE/7XOhd4qB8qP1+nAzT//Mp8LdkNokZgXDtisd62vEj8nizaWmI1RhgylTneR/F8oYeMvDUXPAHIXHOQtXCgHfuoRem3622M0bDMHj3+GTL12DSmUCf/hhrpRU3/mC9ppt92MbVeTBxt7Rvrow2/oSVn1NFmtw0W7whK59dE1FTNiUOLQsNcGkLNHCv+Ra5dgYb4l49g9rW5hxT7PBLSZqEhhq7trBbqfXQzxVzroqxs8D6w7wI5+L+XaZfEP0d9sLZLHx7ndeld3VSC+39mUFaMbOs4QYkm/BnGP6TCRlw/Tt1exouuPGCpxPo1JpB4kjsN6j86DzyudHoEzrOJo++PVWSbqeP5jzjA7TQEugdFoUVIUqZIlQgleMZQDz+DexgcAyIBPMHoQlkCaQ4Aqzaf+DwLZVkV1OxOlgAW9hIexFS0d0utaXXLy9Cxgbe4b4vc1OJa+pmtuzQbOh6lu4rmy1DZ1RG5GXpaCrOhTVnUOtjHueeFae1wZ7V2UrUWheZb/D4RILGVJCy60ik3xjyhtQaQtig/ggiR9tVNrUyR5R+idp6Bt83HNfQGdvfF0KCku7qJ0EiY2TeoZ0OBScqwJFDedIHqydngMsezH6r9hLWTkD2uxQ71YoZ1l+7zsvgJstjIuloH4TuuAaJKqEvhO9hml6mxqJRozUbRNyR5IK
x-ms-exchange-antispam-messagedata-1: Pr6yWtXxM8vg+A==
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
X-OriginatorOrg: cs.auckland.ac.nz
X-MS-Exchange-CrossTenant-AuthAs: Internal
X-MS-Exchange-CrossTenant-AuthSource: SY9P300MB881477.AUSP300.PROD.OUTLOOK.COM
X-MS-Exchange-CrossTenant-Network-Message-Id: a31eb61a-bf23-47a6-3a31-08df396cfaf6
X-MS-Exchange-CrossTenant-originalarrivaltime: 03 Nov 2026 05:40:33.9218 (UTC)
X-MS-Exchange-CrossTenant-fromentityheader: Hosted
X-MS-Exchange-CrossTenant-id: d1b36e95-0d50-42e9-958f-b63fa906beaa
X-MS-Exchange-CrossTenant-mailboxtype: HOSTED
X-MS-Exchange-CrossTenant-userprincipalname: xYry92nFV6/c6wWGNkj5pzyg+Y5gfaGTNYVRBTXoTo3MozEtKdxhtI1SsXR0buflgWpu+CzuhROCAtmRwUAoxwoYmekGs+y8bjMMn2993fU=
X-MS-Exchange-Transport-CrossTenantHeadersStamped: ME0P300MB0445
X-Spamd-Bar: -------------------
X-Original-From: Peter Gutmann <pgut001@cs.auckland.ac.nz>
Message-ID-Hash: GSYKBESELRATUG6T2EKMDXMKS5OZ5B74
X-Message-ID-Hash: GSYKBESELRATUG6T2EKMDXMKS5OZ5B74
X-MailFrom: forwardingalgorithm@dmarc.ietf.org
X-Mailman-Rule-Misses: dmarc-mitigation; no-senders; approved; loop; banned-address; header-match-cfrg.irtf.org-0; header-match-cfrg.irtf.org-1; emergency; member-moderation; nonmember-moderation; administrivia; implicit-dest; max-recipients; max-size; news-moderation; no-subject; digests; suspicious-header
X-Mailman-Version: 3.3.10
Precedence: list
Subject: [CFRG] Re: Stop Calling Them Provers: The Case for Calling ProVerif and Tamarin Symbolic Protocol Analyzers
List-Id: Crypto Forum Research Group <cfrg.irtf.org>
Archived-At: <https://mailarchive.ietf.org/arch/msg/cfrg/f6xYQeF-XrsShvK32VJEqTgzOTM>
List-Archive: <https://mailarchive.ietf.org/arch/browse/cfrg>
List-Help: <mailto:cfrg-request@irtf.org?subject=help>
List-Owner: <mailto:cfrg-owner@irtf.org>
List-Post: <mailto:cfrg@irtf.org>
List-Subscribe: <mailto:cfrg-join@irtf.org>
List-Unsubscribe: <mailto:cfrg-leave@irtf.org>

Ilari Liusvaara <ilariliusvaara@welho.com> writes:

>And sometimes there is also excess complexity to make formal validation
>easier.

A variant of this is where a small change or potential fix can't be applied
because the formal validation can't handle it, a variation of the FIPS 140
problem where you have the choice of certified-secure crypto with exploitable
vulnerabilities or no-longer-certified-secure crypto with the vulnerabilities
fixed.  This tail-wagging-the-dog happened recently with some change in TLS
1.3 that couldn't be made because the formal validation wouldn't handle it.

Apart from formal analysis, sophisticated enough AI models can also do an
amazing job at pointing out issues with protocols.  For example the total
dog's breakfast that is CMP can never be formally verified but an AI can look
at it and point out problem after problem that neither humans (because it's
too complex) nor formal methods (because it can't be analysed through them)
would ever discover.

Peter.

v2.46.0 | Report a Bug | By Email | System Status