DeepSec 2.0.0 Official release

We're officially releasing DeepSec 2.0.0 and DeepSec UI 1.0.0.

We would like to give our many thanks to everyone that participated in the beta phase. We corrected several bugs (see changelog) and added a missing display functionality: the option --trace in command line.

See DeepSec UI Github to download and install DeepSec UI 1.0.0

DeepSec 2.0.0 Beta

We're entering the beta phase ! There should not be any new feature up to the official release. We will mainly focus on fixing bugs.

Changelog:

• The memory consumption of DeepSec has been reduced (up to 4 times less memory).
• Better integration with DeepSec UI Alpha RC3
• Fix many bugs
• A User Error is given when entering an improper dps file instead of an internal error.

DeepSec 2.0.0 Alpha

DeepSec 2.0.0 is a major rework of DeepSec. It is still a command-line tool but it can also be used with the new user interface DeepSec UI. See DeepSec UI Github to download and install DeepSec UI 1.0.x . Amongst the new features of both DeepSec and DeepSec UI:

• Improved efficiency when verifying queries.

• Support for "Eavesdrop", "Classic" and "Private" semantics (POST'17)
  for verifying trace equivalence.

• Integration and improvements of session equivalence (CCS'19).

• Recording of the result of your runs that can be displayed in DeepSec UI.

• DeepSec UI supports all of DeepSec's abilities does but with a nice
  interface.

• Interactive display of attacks for violated queries.

• Attack and equivalence simulators in DeepSec UI for trace equivalence:
  when a trace equivalence query holds, you can select a trace on any of
  the two processes and request an equivalent trace; when violated there
  is an attack trace on one of the processes, and you can select any trace
  on the other process to see why they are not equivalent. Note that these
  simulators only work with trace equivalence and not session equivalence.

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:

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.