Skip to content

DeepSec initial release

Compare
Choose a tag to compare
@VincentCheval VincentCheval released this 19 Dec 09:05
· 563 commits to master since this 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:

  1. 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.
  2. 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.
  3. 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
  4. 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.