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

Application domain/field

• Security protocol analysis
• Cryptographic protocols

Type of tool

Security protocol verifier

Expected input

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

Format:

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).

Internals

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

Comments

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