Install
Manual
Source code
Publications
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 is a verification tool which allows verification of trace equivalence and equivalence by session for a large variety of user defined cryptographic primitives—those that can be represented by a subterm convergent destructor rewrite system.
Team
Vincent Cheval, Steve Kremer, Itsaka Rakotonirina, Victor Yon
Current maintainer: Vincent Cheval
A mailing list is also available for general discussions on DeepSec and announcements of new releases.
- To subscribe, send an email to
sympa@inria.frwith subjectsubscribe deepsec <your first name> <your last name> - To post on the mailing list once subscribed, send an email to
deepsec@inria.fr
Documentation
The DeepSec user manual is available here.
Source code
Deepsec is an open source project, licensed under the GNU General Public License v3.0. All source code is available here.
Publications
[1] V. Cheval, S. Kremer, and I. Rakotonirina, “DEEPSEC: Deciding equivalence properties in security protocols - theory and practice,” in Proceedings of the 39th ieee symposium on security and privacy (S&P’18), 2018.
[2] V. Cheval, S. Kremer, and I. Rakotonirina, “The deepsec prover,” in Proceedings of the 30th International Conference on Computer Aided Verification, Part II (CAV’18), 2018.
[3] V. Cheval, S. Kremer, and I. Rakotonirina, “Exploiting symmetries when proving equivalence properties for security protocols,” in Proceedings of the 26th ACM Conference on Computer and Communications Security (CCS’19), 2019, pp. 905–922.
[4] K. Babel, V. Cheval, and S. Kremer, “On the semantics of communications when verifying equivalence properties,” Journal of Computer Security, vol. 28, no. 1, pp. 71–127, 2020.
