SAT-Equiv

SAT-Equiv is a free equivalence checker for cryptographic protocols. It proceeds by reduction to planning problem and SAT-formula. The new version is efficient enough to handle hundreds of sessions and sometimes reach unboundedness thresholds.

This tool has been described in our papers (see below for example files and sources):

Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Efficiently deciding equivalence for standard primitives and phases, to appear at ESORICS'18 (PDF (long)).
Véronique Cortier, Antoine Dallon, 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. (PDF, PDF (long), BibTeX + Abstract).

The long version is also available here.

Sources

SAT-Equiv 0.1 (CSF'17 version)
SAT-Equiv 0.2
SAT-Equiv 0.3 (ESORICS'18 version).

Installation

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.3.tar.gz
Inside the SAT-Equiv directory, run make. You will need a recent version of OCaml (version 4.04.2 is known to work).
The executable program satequiv has been built.
You can test ./satequiv Examples/Denning-Sacco-B/ds-3.pi which should give you a quick answer.
A list of options is available through ./satequiv --help.
More information can be found in the README file.

Feel free to ask any unanswered question to name@lsv.fr where name is dallon.

License

SAT-Equiv is distributed under the GNU AGPL License.

Benchmarks

Other tools

The tools referenced in the benchmark are (versions are those used for the ESORICS'18 paper):

SPEC (Version 0.3, as on January 18th, 2017);
Akiss (as on October 24th, 2017);
Deepsec (as on April 22th, 2018);
SAT-Equiv 0.1 and 0.3.

Experimental results

The benchmarked were stopped for three reasons:

Time Out (TO) after more than 24h;
Memory Out (MO) when more than 128Go RAM were used;
Stack Overflow (SO) when a Stack Overflow exception was raised.

We provide two result tables. Others are available in the long version (see above).

A symmetric example: the Yahalom-Paulson protocol

	SPEC	Akiss	Deepsec	v. 0.1 (CSF'17)	v. 0.3 (ESORICS'18)
3	23m	7s	10ms	50s	400ms
6	MO	TO	900ms	165m	5s
7			6s	TO	17s
10			85m		63s
12			TO		143s
14					6m
21					155m
28					7h

An assymmetric example: the Active Authentication protocol

	SPEC	Akiss	Deepsec	SAT-Equiv
4	15m	3s	0s	0.01s
6	MO	5m	0.02s	0.07s
8		SO	0.02s	0.07s
46			23h50m	0.9s
50			TO	1.1s
80				3s
200				18s
400				78s

Example files

Example files for my PhD thesis are available here.
ESORICS'18 example files are available here. SAT-Equiv example files are also provided with the tool.
CSF'17 benchmark files for SAT-Equiv, APTE, AKISS and SPEC can be found in this link.