The Squirrel Prover is a proof assistant for protocols, based on first-order logic and provides guarantees in the computational model