Local mirror of Automated Stateful Protocol Verification entry of the Archive of Formal Proofs (AFP).
Não pode escolher mais do que 25 tópicos Os tópicos devem começar com uma letra ou um número, podem incluir traços ('-') e podem ter até 35 caracteres.
Achim D. Brucker 140ae6d623 Import of AFP for Isabelle 2021. há 1 mês
Automated_Stateful_Protocol_Verification Import of AFP for Isabelle 2021. há 1 mês
CITATION Added CSF 2021 paper. há 3 meses
LICENSE Initial commit, based on AFP entry dated 2020-05-22. há 10 meses
README.md Added CSF 2021 paper. há 3 meses


Automated Stateful Protocol Verification

This git repository contains a local mirror of Stateful Protocol Composition and Typing entry of the Archive of Formal Proofs (AFP).

The official AFP releases are tagged. Additionally, this repository may contain extensions (i.e., a development version) that may be submitted (as an update of the Automated Stateful Protocol Verification entry) at a later stage.


This project depends on another AFP entry: Stateful Protocol Composition and Typing. Please follow the official guidelines for installing the AFP locally. For short:

  • Download the complete AFP
  • Extract the downloaded archive to an directory of your choice
  • Let’s assume the extracted archive lives in /home/isabelle/afp, now execute:
achim@logicalhacking:~$ echo "/home/isabelle/afp/thys" >> ~/.isabelle/Isabelle2020/ROOTS

How to build

achim@logicalhacking:~$ isabelle build -D Automated_Stateful_Protocol_Verification



This project is licensed under a 3-clause BSD-style license.

SPDX-License-Identifier: BSD-3-Clause

Master Repository

The master git repository for this project is hosted by the Software Assurance & Security Research Team at https://git.logicalhacking.com/afp-mirror/Automated_Stateful_Protocol_Verification.