[Ufmrg] bugs in formal methods software
Gergely Buday <g.buday@sheffield.ac.uk> Fri, 08 September 2023 13:40 UTC
Return-Path: <g.buday@sheffield.ac.uk>
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 2761AC151069 for <ufmrg@ietfa.amsl.com>; Fri, 8 Sep 2023 06:40:17 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -0.208
X-Spam-Level:
X-Spam-Status: No, score=-0.208 tagged_above=-999 required=5 tests=[BAYES_20=-0.001, DKIMWL_WL_MED=-0.001, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_ZEN_BLOCKED_OPENDNS=0.001, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01, 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=sheffield.ac.uk
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 V8C0DY3KbtqI for <ufmrg@ietfa.amsl.com>; Fri, 8 Sep 2023 06:40:12 -0700 (PDT)
Received: from mail-lf1-x130.google.com (mail-lf1-x130.google.com [IPv6:2a00:1450:4864:20::130]) (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 47145C151064 for <Ufmrg@irtf.org>; Fri, 8 Sep 2023 06:40:08 -0700 (PDT)
Received: by mail-lf1-x130.google.com with SMTP id 2adb3069b0e04-501cba1ec0aso3449837e87.2 for <Ufmrg@irtf.org>; Fri, 08 Sep 2023 06:40:08 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sheffield.ac.uk; s=170424.google; t=1694180406; x=1694785206; darn=irtf.org; h=to:subject:message-id:date:from:mime-version:from:to:cc:subject :date:message-id:reply-to; bh=e68oSDiOK1dA/JK7siIpff5qfxBjWZm5vDLV7lO3WiM=; b=KJu1tUnCXHE+Ry7kyWR/fEGMtQ9PaM6yApud4rqLGLo0a3Wj0Ns/xX63Xw/pPeEDOU bQ/rMsPtUOkXOOW0ADcPBbiTriCSVwJq+LpbYKkhmETQ1QpHP62fKqTQ4rIu3lps5vGR jd2HBaBc6OnaOUTIyMJZmviwkIf0ngDSb227u9PDgDaEBu66un7n2VLIDh44nQeeU3JT Q/CkJMRaCuzvwjPdGjAQeo1IRhqcAfQxk+NS5+JQ4/CX3aZ+hCwIsvC+t8Q6VXd3h3qE Ps40e8jaPybfH0c3IZwv2HKrQpT14B52nwcBw/Axf4gfxU2i4MZDC09ptYXKZEn7s+wm wC1A==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1694180406; x=1694785206; h=to:subject:message-id:date:from:mime-version:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=e68oSDiOK1dA/JK7siIpff5qfxBjWZm5vDLV7lO3WiM=; b=lhTLN9LCH7CuMmXQ1A0HhHwmWnKlSOpPbPm7uP+7DaSh0/JLe9OEE/QY+ryZgwIJcZ Ntev64FMAu6Xf0mxX1ssHMbkTsIOgvii4o4ij2/iSlY7CViWtqh2/yGAKdSwbZSiRkhn cXXylKMKunpHHjwQ/5h5kD4LcvGyEDti3gJ2LpwSWoqYJHjWkF7NkPQLQjVmqUxUrt+S FSgKWjHEJfENYVAb7hmAF9u303HrJ5OWR7TFzNerX2U4cbPxbG2i6PUZjHFtN9+/N2As pKr0xcI4JkWp7SIROqz0cnB8umjmq/l9MQSCw/iXiH8r8dkbq8Cpf718w/ReG0G5LHIK Obrw==
X-Gm-Message-State: AOJu0Yzfq/cnLdns2zOlLy54+KvsIpkzLEde8mjeQnEw3Yl2BXFwZMLI VpF82Nw/xczKmw22amBk9nb3TBgtRwnwghkMGkCQioCJLJEZjyXrKJl+TKlb1A3PDkrZ5k5hQ2E li8JspO4HPuXsqSCspCctmzqvA5anA1kvFsFGEn+32EjPAjheA2zeIXzRLbntwLxiC2OPlnRMhs QspHtMRatwE0LkjCESMQ==
X-Google-Smtp-Source: AGHT+IF5vqA5MYTGqfW9mel5+qGUOmrYq+niNM/WBVT921QNqUu2Isqnvc0ENPbjqNSdEV3EBJogqHb/Tl6D+Dl3/Yw=
X-Received: by 2002:ac2:4c48:0:b0:4fe:49d:6ae2 with SMTP id o8-20020ac24c48000000b004fe049d6ae2mr2337619lfk.0.1694180406149; Fri, 08 Sep 2023 06:40:06 -0700 (PDT)
MIME-Version: 1.0
From: Gergely Buday <g.buday@sheffield.ac.uk>
Date: Fri, 08 Sep 2023 14:39:55 +0100
Message-ID: <CAHgAKgQQCyoLuOXpv_YbiYhT-typqc8Apx59D_rGj7cNtA4VwQ@mail.gmail.com>
To: nadim@symbolic.software, Ufmrg@irtf.org
Content-Type: multipart/alternative; boundary="0000000000004bb48e0604d91de8"
Archived-At: <https://mailarchive.ietf.org/arch/msg/ufmrg/RxwCnvlkditB43m27-y1v98pXwI>
Subject: [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 13:40:17 -0000
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
- [Ufmrg] bugs in formal methods software Gergely Buday
- Re: [Ufmrg] bugs in formal methods software Muhammad Usama Sardar
- Re: [Ufmrg] bugs in formal methods software Nadim Kobeissi