Manual of DeepSec

The manual of DeepSec is also available in PDF.

Table of content

  1. Introduction
  2. Installation
  3. Tutorial
  4. Advanced options
  5. Graphical User Interface
  6. Command-line options
  7. Input grammar

Introduction

The DeepSec prover is a verification tool for cryptographic protocols. It allows the verification of security properties (expressed as trace equivalence) of protocols described in the applied pi calculus. The tool operates in the so-called “bounded number of sessions” model: while it only allows to specify a fixed number of participants and sessions, termination is always guaranteed (though computational resources may be exhausted in practice if the model is too large).

Scope of this manual

This manual provides a “hands-on” introduction on how to use the tool. It provides intuitive explanations of the language and the properties it permits to verify. It also explains the different options and provides a reference guide for the precise syntax. It however does not give formal semantics nor explains the underlying algorithms. The theory underlying DeepSec is yet described in [1] and [2]. Some of the implementation choices are also discussed in a tool paper [3].

Support

Please report any bugs to vincent.cheval@inria.fr or file an issue on our github.

Acknowledgements

The research that led to DeepSec was primarily supported by ERC under the EU’s H2020 research and innovation program (grant agreements No 645865-SPOOC), as well as from the French ANR projects SEQUOIA (ANR-14-CE28-0030-01) and TECAP (ANR-17-CE39-0004-01).

[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, “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.

[3] 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.

 
Top
Installation →