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.