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.