[TLS] Formal analysis of Exported Authenticators
Jonathan Hoyland <jonathan.hoyland@gmail.com> Mon, 26 March 2018 19:04 UTC
Return-Path: <jonathan.hoyland@gmail.com>
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 903591276AF for <tls@ietfa.amsl.com>; Mon, 26 Mar 2018 12:04:42 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -1.999
X-Spam-Level:
X-Spam-Status: No, score=-1.999 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, FREEMAIL_FROM=0.001, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no
Authentication-Results: ietfa.amsl.com (amavisd-new); dkim=pass (2048-bit key) header.d=gmail.com
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 iwjzp_GARffY for <tls@ietfa.amsl.com>; Mon, 26 Mar 2018 12:04:39 -0700 (PDT)
Received: from mail-ua0-x229.google.com (mail-ua0-x229.google.com [IPv6:2607:f8b0:400c:c08::229]) (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 67B6E1272E1 for <tls@ietf.org>; Mon, 26 Mar 2018 12:04:39 -0700 (PDT)
Received: by mail-ua0-x229.google.com with SMTP id o34so9929147uae.9 for <tls@ietf.org>; Mon, 26 Mar 2018 12:04:39 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to; bh=pdFBBSSnS/+4k0PJ84h24eZB2RSrNDiSNqOr/lS9h6E=; b=br+Bv8LH7nYN4nWrc+o/cD07lXcYHv6TFF6vKO9hYZoE/Yrr6WYrv62QPkS0zDkZ1Q BY76zxfepS9IAunkWFhJNFQX1MY8ljsuosxELf47g2i+65wAx9a4kUNtFdq2nuotzYW8 X4Jzo5s9apz3c/822Z+KH7BzO2448/8BBJK7O7/Cv5A4I3veGIdQ2CUrh9ZdjTbBzGn5 txidB4491gkiXUR7qnA+VbdaLOJteJZzvdM3l3AhNQ/aEYCO7Kjt8ROce1vqyRlur3LN hstY7kLCCjqD0ty4pHEcqx+aDhI0UPhgGnD1qVDN/fuo+xGnaarpOw5nf2We6k1+uTTi oW6w==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:from:date:message-id:subject:to; bh=pdFBBSSnS/+4k0PJ84h24eZB2RSrNDiSNqOr/lS9h6E=; b=uLm9aK2LAvx6HUzS+Wed+iWk34cIvTiO2lxmQALerk2CejRxj0wZNfM9tffAy8MHx3 eI9YVgrbfONGTkH3ar2Yl1zJCxdyvAz8acZAgrOp7JnHNCgElBOygMOOvYDOLfTYz8ON nWn0hxtDUz5hEYLyIotEXsFEpTHBRfdjKtm6rJ/Y3+xzLXOsY7dl6rTXPHTaV4k+J1d7 XJTtYIs1rwanRabjeCf4JU6FFVs3erzgDeDMrcXClQ9JogjvyJNW4tTXxMpHpLAP2ZIO bXYz7r28h7sn+5PGnsOkoF37bc1tlkVj3AWg9VZmxEKGmtM6yFJ1m8kfoCYQthlEW0k8 iIZA==
X-Gm-Message-State: AElRT7H+ul7xkc5ybWYxwPFY5kmdQCLdhfJem4t3zsF08MRTJT+CqFiJ yn5BJI7lxoQwrYJjiqje12x5M4D6BdccFXyjlRG/eA==
X-Google-Smtp-Source: AIpwx48sdxHiO3ETDdA818ObCRFQY4MQjmIisQbZYyqdYwmfw+DyUU2qhQJ63Whse7V5w/P6Kun2XtkOo9wWYw7gdyE=
X-Received: by 10.176.36.196 with SMTP id k4mr5860862uan.6.1522091078194; Mon, 26 Mar 2018 12:04:38 -0700 (PDT)
MIME-Version: 1.0
From: Jonathan Hoyland <jonathan.hoyland@gmail.com>
Date: Mon, 26 Mar 2018 19:04:27 +0000
Message-ID: <CACykbs1yutCEhUDVF18QNutsK6jwrh5zw0tcRB3A9JrGqdLZAA@mail.gmail.com>
To: tls@ietf.org
Content-Type: multipart/alternative; boundary="94eb2c1ea354081cb60568557262"
Archived-At: <https://mailarchive.ietf.org/arch/msg/tls/gNtopj6zU795Ourl8kE2BOWjvAU>
Subject: [TLS] Formal analysis of Exported Authenticators
X-BeenThere: tls@ietf.org
X-Mailman-Version: 2.1.22
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, 26 Mar 2018 19:04:43 -0000
Hi all, A number of people expressed interest in the Tamarin model we made of Exported Authenticators. For those interested, you can see the code, along with an explanatory guide here <https://bitbucket.org/jhoyla/tamarin-exported-authenticators>[0]. The full analysis report is a work-in-progress which we hope to release soon. If you have an questions, please feel free to email me. Regards, Jonathan [0] https://bitbucket.org/jhoyla/tamarin-exported-authenticators/overview
- [TLS] Formal analysis of Exported Authenticators Jonathan Hoyland