PV1 DEEPSEC: Deciding Equivalence Properties in Security Protocolschecks whether two cryptographic protocols are trace equivalent

Application domain/field

Type of tool

Security protocol verifier

Expected input

Cryptographic primitives, the protocol and the security properties that should be verified.


Its own .dps format

Expected output

Whether two specified processes are trace equivalent or not. If the query is not satisfied, the interface shows "how to mount the attack" (i.e. a counterexample).


DEEPSEC decides trace equivalence for cryptographic protocols specified in a dialect of the applied pi calculus.


The analysis is restricted to a finite number of protocol sessions.
Protocol Security


Related papers

Last publication date

4 February 2020

Related tools

Other security verifiers: SPEC, APTE, Akiss, Sat-Eq,

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.