Automated verification has become an essential part in the security evaluation of cryptographic protocols. Recently, there has been a considerable effort to lift the theory and tool support that existed for reachability properties to the more complex case of equivalence properties. DeepSec allows you to decide trace equivalence and session equivalence for a large variety of cryptographic primitives---those that can be represented by a subterm convergent destructor rewrite system.
More information on DeepSec is available on its website: https://deepsec-prover.github.io/
A mailing list is available for general discussions on DeepSec and announcements of new releases.
- To subscribe, send an email to sympa@inria.fr with subject "subscribe deepsec " (remove the quotes).
- To post on the mailing list once subscribed, send an email to deepsec@inria.fr
The user manual (html and pdf) is available at: https://deepsec-prover.github.io/manual/