Previous | 
Home
Section: New Software and Platforms
Deepsec
DEEPSEC - DEciding Equivalence Properties in SECurity protocols
Keywords: Security - Verification
Functional Description: DEEPSEC (DEciding Equivalence Properties in SECurity protocols) is a tool for verifying indistinguishability properties in cryptographic protocols, modelled as trace equivalence in a process calculus. Indistinguishability is used to model a variety of properties including anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks, etc. DEEPSEC implements a decision procedure to verify trace equivalence for a bounded number of sessions and cryptographic primitives modeled by a subterm convergent destructor rewrite system. The procedure is based on constraint solving techniques. The tool also implements state-of-the-art partial order reductions and allows to distribute the computation on multiple cores and multiple machines.
News Of The Year: In 2019, to improve efficiency for non-determinate processes, we developed new optimisation techniques. This is achieved through a new, stronger equivalence for which partial-order reductions are sound even for non-determinate processes, as well as new symmetry reductions. We demonstrated that these techniques provide a significant (several orders of magnitude) speed-up in practice, thus increasing the size of the protocols that can be analysed fully automatically. Even though the new equivalence is stronger, it is nevertheless coarse enough to avoid false attacks on most practical examples.
-
Participants: Steve Kremer, Itsaka Rakotonirina and Vincent Cheval
-
Publications: Exploiting Symmetries When Proving Equivalence Properties for Security Protocols - Exploiting symmetries when proving equivalence properties for security protocols (Technical report) - DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice - DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice - The DEEPSEC prover