DeepSec initial release
This is the initial version of the DeepSec tool. The underlying theory is described in [2] and [3]
Main features:
- Verification of trace equivalence between processes
- Support for classical and private semantics (see [1] for details)
- Support user-defined cryptographic primitives expressed as a subterm convergent destructor/constructor rewrite system.
- Partial-order reduction for determinate processes (see [4] for details)
- Distributed and parallel computation
References:
- K. Babel, V. Cheval and S. Kremer. On Communication Models When Verifying Equivalence Properties. In Proceedings of the 6nd International Conference on Principles of Security and Trust (POST'17), Springer Berlin Heidelberg, 2017.
- V. Cheval, S. Kremer and I. Rakotonirina. The DEEPSEC prover. In Proceedings of the 31th International Conference on Computer Aided Verification (CAV'18), Springer, 2018.
- 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), IEEE Computer Society Press, 2018
- D. Baelde, S. Delaune and L. Hirschi. Partial Order Reduction for Security Protocols. In CONCUR'15, Leibniz International Proceedings in Informatics 42, pages 497-510. Leibniz-Zentrum für Informatik, 2015.