SPEC: An equivalence checker for the spi-calculus
SPEC (for Spi-calculus Equivalence Checker) is an equivalence checker
for a version of Abadi and Gordon's spi-calculus. The spi-calculus has
been used to encode security protocols and, via a notion of
observational equivalence, been used to reason about security
properties such as secrecy and authentication.
SPEC implements a process equivalence checking procedure based on the
paper
by Alwen Tiu and Jeremy Dawson (presented in the IEEE Computer
Security Foundations symposium in 2010).
SPEC is implemented on top of a modified version of the
Bedwyr logical
framework.
The modified Bedwyr codes are included in this distribution.
Downloading and installing SPEC
The current version of SPEC is currently still in an alpha-testing
phase. More features will be made available in the future.
- Source code for SPEC version 0.1: spec-0.1.tar.gz.
To install, uncompress it and follow the instructions in the README file.
- Check out the user manual on how to use SPEC.
The manual is also included in the tar.gz file.
Comments and suggestions
I would welcome comments and suggestions. Please email them to alwen.tiu at anu.edu.au.
Acknowledgment
This work is supported by the ARC Discovery grants DP0880549 and DP110103173.
I would like to thank David Baelde for many useful correspondences
regarding the implementation of the Bedwyr system.