In this paper we describe the DeepSec prover, a tool for security-protocol analysis deciding equivalence properties, modelled as trace equivalence of two processes in a dialect of the applied pi calculus.