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:

The long version is also available here.

A new version of SAT-Equiv has been submitted to ESORICS'18. More informations on the submission webpage.

Sources

Installation

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):

Experimental results

The benchmarked were stopped for three reasons:

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

A assymmetric example: the Active Authentication protocol

SPEC AkissDeepsec 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