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

The long version is also available here.



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


SAT-Equiv is distributed under the GNU AGPL License.


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

An 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