DeepSec-prover / deepsec

DEciding Equivalence Properties in SECurity protocols
GNU General Public License v3.0
16 stars 2 forks source link
deepsec destructor-subterm-convergents equivalence-properties

DeepSec: Deciding Equivalence Properties in Security Protocols

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 allows you to decide trace equivalence and session equivalence for a large variety of cryptographic primitives---those that can be represented by a subterm convergent destructor rewrite system.

Website

More information on DeepSec is available on its website: https://deepsec-prover.github.io/

Mailing list

A mailing list is available for general discussions on DeepSec and announcements of new releases.

User manual

The user manual (html and pdf) is available at: https://deepsec-prover.github.io/manual/