IETF Logo Mail Archive

Re: [Ufmrg] bugs in formal methods software

Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de> Fri, 08 September 2023 15:48 UTC

Return-Path: <muhammad_usama.sardar@tu-dresden.de>
X-Original-To: ufmrg@ietfa.amsl.com
Delivered-To: ufmrg@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id D4BD5C14CE44; Fri, 8 Sep 2023 08:48:52 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -2.105
X-Spam-Level:
X-Spam-Status: No, score=-2.105 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, 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 (2048-bit key) header.d=tu-dresden.de
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 bkI7xqXMZ5Cd; Fri, 8 Sep 2023 08:48:48 -0700 (PDT)
Received: from mailout3.zih.tu-dresden.de (mailout3.zih.tu-dresden.de [141.30.67.74]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange ECDHE (P-256) server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by ietfa.amsl.com (Postfix) with ESMTPS id 44F0CC151080; Fri, 8 Sep 2023 08:48:47 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=tu-dresden.de; s=dkim2022; h=MIME-Version:Content-Type:In-Reply-To: References:Message-ID:Date:Subject:To:From:Sender:Reply-To:Cc: Content-Transfer-Encoding:Content-ID:Content-Description:Resent-Date: Resent-From:Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID:List-Id: List-Help:List-Unsubscribe:List-Subscribe:List-Post:List-Owner:List-Archive; bh=hq3hIzNBUCY2lKUdKV8ksRDZ63S0LzeAm2oThqY/XBI=; b=yTnKFe1x//6EtlJrwxntBfv0Lx bpBNYVCLEiVdwLA70gT0Ett1glGczq2+r4RXQ/xcfEMS3l/EhXQiyEtC2yb9CGPP7gtWZ7l5xF651 K3wHDR7R4v0evB2JMdnQH1clmwOW9L4aD4CUOVqWVi8tqZZy1AYwsNql0h3onk2Qdy+qan6VDtBNa NUbI9u576eABUHKqjB/qCslVj8Y+X4z4A8OBP/t21pn7kPwxIu2HZmHLpi38xhuZ1iTqRQzaCu4wy 4XFV0Hus9p0Furp72BTUcdMBYgVjnooz6eXVxwm3zqhPLexWl9QW6TkrEBr1MiDEK+GgMDDVsNwXg nkJkD8gA==;
Received: from [172.26.35.115] (helo=msx.tu-dresden.de) by mailout3.zih.tu-dresden.de with esmtps (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from <muhammad_usama.sardar@tu-dresden.de>) id 1qedS7-00ALbF-OS; Fri, 08 Sep 2023 17:31:24 +0200
Received: from MSX-T314.msx.ad.zih.tu-dresden.de (172.26.35.114) by MSX-T315.msx.ad.zih.tu-dresden.de (172.26.35.115) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.1.2507.31; Fri, 8 Sep 2023 17:31:09 +0200
Received: from MSX-T314.msx.ad.zih.tu-dresden.de ([172.26.35.114]) by MSX-T314.msx.ad.zih.tu-dresden.de ([172.26.35.114]) with mapi id 15.01.2507.031; Fri, 8 Sep 2023 17:31:09 +0200
From: Muhammad Usama Sardar <muhammad_usama.sardar@tu-dresden.de>
To: Gergely Buday <g.buday=40sheffield.ac.uk@dmarc.ietf.org>, "nadim@symbolic.software" <nadim@symbolic.software>, "Ufmrg@irtf.org" <Ufmrg@irtf.org>
Thread-Topic: [Ufmrg] bugs in formal methods software
Thread-Index: AQHZ4loEYOuyqnkJ2E24daiIMuLO+7ARDKVx
Date: Fri, 08 Sep 2023 15:31:08 +0000
Message-ID: <0deef4889098416391db79bde18afc3f@tu-dresden.de>
References: <CAHgAKgQQCyoLuOXpv_YbiYhT-typqc8Apx59D_rGj7cNtA4VwQ@mail.gmail.com>
In-Reply-To: <CAHgAKgQQCyoLuOXpv_YbiYhT-typqc8Apx59D_rGj7cNtA4VwQ@mail.gmail.com>
Accept-Language: de-DE, en-US
Content-Language: de-DE
X-MS-Has-Attach:
X-MS-TNEF-Correlator:
x-pmwin-version: 4.0.4, Antivirus-Engine: 3.87.0, Antivirus-Data: 6.03
Content-Type: multipart/alternative; boundary="_000_0deef4889098416391db79bde18afc3ftudresdende_"
MIME-Version: 1.0
X-TUD-Virus-Scanned: mailout3.zih.tu-dresden.de
Archived-At: <https://mailarchive.ietf.org/arch/msg/ufmrg/Bla9i_kIDU7GevYJMGslGRD8oFw>
Subject: Re: [Ufmrg] bugs in formal methods software
X-BeenThere: ufmrg@irtf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Usable Formal Methods Research Group <ufmrg.irtf.org>
List-Unsubscribe: <https://www.irtf.org/mailman/options/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/ufmrg/>
List-Post: <mailto:ufmrg@irtf.org>
List-Help: <mailto:ufmrg-request@irtf.org?subject=help>
List-Subscribe: <https://www.irtf.org/mailman/listinfo/ufmrg>, <mailto:ufmrg-request@irtf.org?subject=subscribe>
X-List-Received-Date: Fri, 08 Sep 2023 15:48:52 -0000

Hello Gergely,

One of these bugs was found in Verifpal by one of the trainees during the tutorial in Eurocrypt 2021. I don't find it documented, though.


------------------------------------------------------------------------------------------------------------------------------------------
Best Regards,

Muhammad Usama Sardar (M.Sc.)

Research Associate

Technische Universität Dresden


Faculty of Computer Science

Institute of Systems Architecture

Chair of Systems Engineering


Office: APB 3073

Phone: +49 351 463-42048

Email: muhammad_usama.sardar@tu-dresden.de

Website: https://tu-dresden.de/ing/informatik/sya/se/die-professur/beschaeftigte/muhammad-usama-sardar

------------------------------------------------------------------------------------------------------------------------------------------

________________________________
Von: Ufmrg <ufmrg-bounces@irtf.org> im Auftrag von Gergely Buday <g.buday=40sheffield.ac.uk@dmarc.ietf.org>
Gesendet: Freitag, 8. September 2023 15:39:55
An: nadim@symbolic.software; Ufmrg@irtf.org
Betreff: [Ufmrg] bugs in formal methods software

Dear Nadim

at the interim meeting you were talking about discovered bugs in formal methods software for security protocols.

Could you please tell us a few words about these as it is interesting: what kind of bugs are these, where can we read about them and how they influence the use of these tools?

Yours

- Gergely

v2.23.0 | Report a Bug | By Email