SAPIC+
SAPIC+ is a security protocol verification platform, enabling the use of multiple verification tools as possible backends. It currently supports exports to ProVerif, Tamarin and DeepSec. It is directly integrated within Tamarin, which can directly be used to verify the input file, or allows through a command line option to produce a valid input file for either ProVerif or DeepSec.
Documentation
The Tamarin user manual is available here.
The specific SAPIC+ instructions corresponds to the description of the protocol specification using processes. Other relevants parts of the manual include the property specification part, where SAPIC+ uses the same lemma specification as Tamarin (which are in turn automatically translated to Proverif queries).
Installation
Installation instructions for Tamarin (and this SAPIC+) are in the manual.
See the ProVerif and DeepSec website for their corresponding installation instructions. Alternatively, we also provide a Docker, but which may not contain the latest fixes and features.
Research Papers
Papers on SAPIC+ and its theory
- "Sapic+ : protocol verifiers of the world, unite!" [PDF], by Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann: the extension from SAPIC to SAPIC+, introducing the exports to ProVerif and DeepSec . Presented at USENIX Security 2022.
- "Symbolic Models for Isolated Execution Environments. " [PDF], by Charlie Jacomme, Steve Kremer, and Guillaume Scerri: this paper added support for isolated execution environment. Presented at Euro S&P 2017.
- "A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange" [PDF], by Michael Backes, Jannik Dreier, Steve Kremer and Robert Künnemann: this paper added non-deterministic choice, reliable channels and local progress to SAPIC. Presented at Euro S&P 2017.
- "Automated analysis of security protocols with global state." [PDF], by Steve Kremer and Robert Künnemann: the original SAPIC journal paper, introducing the SAPIC input language and its translation to Tamarin's input language. Published in JCS 2016.
Papers using SAPIC+
- "A comprehensive, formal and automated analysis of the EDHOC protocol." [PDF], by Charlie Jacomme, Steve Kremer, Elise Klein, and Maïwenn Racouchot: the first case-study using SAPIC+ to the best of its capabilities, and that helped in the IETF standardization of the EDHOC protocol. Presented at USENIX Security 2023.