SAT-Equiv is a free equivalence checker for cryptographic protocols.
It proceeds by reduction to planning problem and SAT-formula,
for a bounded number of sessions.
This tool has been described in our paper:
- Véronique Cortier,
and Stéphanie Delaune.
SAT-Equiv: an efficient tool for equivalence properties,
in Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17),
Santa Barbara, California, USA, August 2017, pages 481-494.
IEEE Computer Society Press.
BibTeX + Abstract).
The long version is available here
Example files for SAT-Equiv, APTE, AKISS and SPEC
can be found in this link.
- SAT-Equiv performs a reduction to SAT formula,
and feeds minisat with it.
So you should start by installing minisat.
On Debian/Ubuntu, it is sufficient to use
apt-get install minisat.
- Unpack the sources through
tar -zxvf satequiv-0.2.tar.gz
- Inside the SAT-Equiv directory, run
You will need a recent version of OCaml.
- The executable program
satequiv has been built.
- You can test
which should give you a quick answer.
- A list of options is available through
- More information can be found in the README file.
Feel free to ask any unanswered question to email@example.com where name is dallon.