| author |
|
|||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| title | DeepSec prover | |||||||||||||||
| pagetitle | Index | |||||||||||||||
| mainpagetitle | ||||||||||||||||
| navigation | false | |||||||||||||||
| next_page | ||||||||||||||||
| next_page_url | ||||||||||||||||
| prev_page | ||||||||||||||||
| prev_page_url | ||||||||||||||||
| link-citations | true | |||||||||||||||
| nocite | @* |
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.
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
The DeepSec user manual is available here.
Deepsec is an open source project, licensed under the GNU General Public License v3.0. All source code is available here.