Tags:Automatic verification, Behavioural equivalence, Cryptographic protocol, Formal methods, Privacy-type properties, Security and Symbolic model
Abstract:
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.
