[Lake] Fwd: [irtf-discuss] Usable formal methods side meeting at IETF 115
Colin Perkins <csp@csperkins.org> Fri, 04 November 2022 16:56 UTC
Return-Path: <csp@csperkins.org>
X-Original-To: lake@ietfa.amsl.com
Delivered-To: lake@ietfa.amsl.com
Received: from localhost (localhost [127.0.0.1]) by ietfa.amsl.com (Postfix) with ESMTP id 8BD1DC1522A0; Fri, 4 Nov 2022 09:56:46 -0700 (PDT)
X-Virus-Scanned: amavisd-new at amsl.com
X-Spam-Flag: NO
X-Spam-Score: -7.105
X-Spam-Level:
X-Spam-Status: No, score=-7.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_DNSWL_HI=-5, 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=csperkins.org
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 WCzvOaBPXMHX; Fri, 4 Nov 2022 09:56:41 -0700 (PDT)
Received: from mx2.mythic-beasts.com (mx2.mythic-beasts.com [IPv6:2a00:1098:0:82:1000:0:2:1]) (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 8874CC14CE32; Fri, 4 Nov 2022 09:56:41 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=csperkins.org; s=mythic-beasts-k1; h=Date:Subject:To:From; bh=jqs0S4jqMXhD87b1Cn14E4lVJfJHvEnYPr1k2phNbt8=; b=1MwcFT+E+hC5rPmgab/ICX3Nb/ +B1xZ3ng/tLl56baEW9z7qLgpsMXIiTxlIcIpagfqbkxUrHs2qCG4sch7oOq5Ntw41WA3X/u27/5W X2S/0Yr8FrGIokyenuBvj7W6x1c0HTCZtlpA6Q7GuBCtn9izWwSz487rbf956idCnQfBhHNTe5fvU sPBKtdP9l8bfHJKhQvNaKWgWnPj31EiOmqqWdqtbGKekxwstnv2sRrKActTt3v8TNVJpxL1f7CynB 9jbFNI2063kIEGhizTdCT4dh4X1WCQdiXJTWetXvxDXiCmlXNhoAceN/zxgyz0ynEAc7O+C5+c7eT /ZdifLFQ==;
Received: from [81.187.2.149] (port=45382 helo=[192.168.56.1]) by mailhub-hex-d.mythic-beasts.com with esmtpsa (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from <csp@csperkins.org>) id 1oqzzj-0003uP-9u; Fri, 04 Nov 2022 16:56:39 +0000
From: Colin Perkins <csp@csperkins.org>
To: lake@ietf.org, tls@ietf.org
Date: Fri, 04 Nov 2022 16:56:35 +0000
Reply-To: irtf-discuss@irtf.org
X-Mailer: MailMate (1.14r5926)
Message-ID: <1E66C3F8-63BA-47AC-AC40-E2AE6ED28660@csperkins.org>
References: <C91D3863-37D3-4E09-B1F9-588C316240CD@csperkins.org>
MIME-Version: 1.0
Content-Type: multipart/alternative; boundary="=_MailMate_CA7A411F-9125-41BE-AD2B-74383367B2F2_="
X-BlackCat-Spam-Score: 0
Archived-At: <https://mailarchive.ietf.org/arch/msg/lake/SoopQxThggHqOJ6chbSPW00QnNY>
Subject: [Lake] Fwd: [irtf-discuss] Usable formal methods side meeting at IETF 115
X-BeenThere: lake@ietf.org
X-Mailman-Version: 2.1.39
Precedence: list
List-Id: Lightweight Authenticated Key Exchange <lake.ietf.org>
List-Unsubscribe: <https://www.ietf.org/mailman/options/lake>, <mailto:lake-request@ietf.org?subject=unsubscribe>
List-Archive: <https://mailarchive.ietf.org/arch/browse/lake/>
List-Post: <mailto:lake@ietf.org>
List-Help: <mailto:lake-request@ietf.org?subject=help>
List-Subscribe: <https://www.ietf.org/mailman/listinfo/lake>, <mailto:lake-request@ietf.org?subject=subscribe>
X-List-Received-Date: Fri, 04 Nov 2022 16:56:46 -0000
There’s a side meeting on usable formal methods for protocol specification taking place during IETF next week that may be of interest to some in this group – please consider attending. Colin Forwarded message: > From: Colin Perkins <csp@csperkins.org> > To: irtf-discuss@irtf.org > Cc: 115attendees@ietf.org > Subject: [irtf-discuss] Usable formal methods side meeting at IETF 115 > Date: Fri, 04 Nov 2022 16:42:21 +0000 > > Hi, > > How should we describe and specify protocols? > > How can we ensure that network protocol specifications are consistent > and correct, and verify that implementations match the specification? > > The IETF community has long used natural language, English, to > describe and specify its protocols, with occasional use of formal > languages and a some limited amounts of formal verification. One of > the sessions in the Applied Networking Research Workshop at IETF 114 > [1] started to discuss whether this is the right approach, and to what > extent formal methods, structured specification languages, and natural > language processing techniques can help describe network protocols. > > Chris Wood and I are organising a side meeting at IETF 115 to continue > this discussion, and to assess interest in forming a new IRTF research > group to explore usable formal methods for protocol specification. > > This will takes place on Thursday lunchtime, 10 November, from > 11:30-13:00 UK time in room Richmond 5 of the IETF meeting hotel (the > IAB breakout room). > > The draft agenda is as follows: > > - Welcome, Goals, Motivation, Introductions > - (15 mins) > - Short presentations (45 mins) > - “What are Formal Methods and Why Should We Care?”Jonathan > Hoyland > - “Formal Specification and Specification-Based Testing of > QUIC”, Ken McMillan > - Discussion of proposed charter (20 mins) > - See [Google > Doc](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#) > - Next steps (10 mins) > - Does this seem appropriate for an RG? > - Are there volunteers to work on this topic? > - What, if anything, have we missed? > > if you’re interested in this topic, please review [the draft > charter](https://docs.google.com/document/d/1X1aFFXg-LTNcT4cpo3FZ6w1PwHG33Q0RAUUf-R7Kmus/edit#) > and come along to the side meeting to give your feedback. > > Hope to see you in London! > > Colin > > > > [1] https://www.youtube.com/watch?v=tCsiB87s-f4 > > -- > Colin Perkins > https://csperkins.org/
- [Lake] Fwd: [irtf-discuss] Usable formal methods … Colin Perkins