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. In this paper we contribute both to the theory and practice of this verification problem. We establish new complexity results for static equivalence, trace equivalence and labelled bisimilarity and propose a new decision procedure for these equivalences in the case of a bounded number of sessions. Our procedure provides the first tool to decide trace equivalence and labelled bisimilarity exactly for a large variety of cryptographic primitives—those that can be represented by a subterm convergent destructor rewrite system. We implemented the procedure in a new tool, DeepSec. We perform an extensive experimental verification showing that our tool is significantly more efficient than many other similar tools, while at the same time raises the scope of the protocols that can be analyzed.
How to install DeepSec?
DeepSec has been successfully tested on Linux and MacOSX (Windows is currently not supported). DeepSec requires OCaml > 4.03. It is highly recommended to install OCaml through
opam instead of a native package manager, such as
apt-get (the latest version on
apt-get may not be the latest release of OCaml).
opam itself may however be safely installed using your favorite package manager (see instructions for installing
Upgrading Ocaml using OPAM
opam switch list(The version 4.05.0 should be displayed in the list. Otherwise run first
opam switch 4.05.0(latest official release)
- Follow the instructions (at the end do not forget to set the environment by running
eval `opam config env`)
Installation of DeepSec
git clone https://github.com/DeepSec-prover/deepsec.git(with a HTTPS connexion) or
git clone email@example.com:DeepSec-prover/deepsec.git(with a SSH connexion)
- Inside the directory
- The executable program
deepsechas been built.
- Add the
deepsecexecutable to your path, e.g. if your shell is bash, add the line
export DEEPSEC_DIR=<path to the deepsec folder>/deepsecto the .bash_profile file
The fourth step is not mandatory but highly recommended. If the variable
DEEPSEC_DIR is not defined,
deepsec can only be used with the option
-deepsec_dir <path to the deepsec folder>/deepsec.
Note that two executable programs are compile at the same time as
manager_deepsec. These executables are used by DeepSec to distribute the computation through multi-core architectures and clusters of computers. They should note be used manually nor should they be moved from the
How to use DeepSec?
To use DeepSec, you first need to specify your security protocol inside a file. The input grammar of DeepSec is very similar to the untyped input grammar of ProVerif. Examples of input files can be found in the DeepSec repository.
Free and privates names can be defined using the keyword
free ca, cb. free c. free ska, skb, skc [private].
Construction function symbols are defined with the keyword
fun. Note that the arity of the function symbol shall be provided.
fun aenc/2. fun pk/1.
Constants can be declared either using the keyword fun or the keyword const.
const ok. fun bad/0.
Destructor function symbols are defined by the rewrite rules that describe their cryptographic behavior, using the keyword
reduc adec(aenc(x,pk(y)),y) = x.
Note that if a destructor function require several rewrite rules, they should be defined inside the same reduc.
reduc exists_double(x,x,y) -> ok; exists_double(x,y,x) -> ok; exists_double(y,x,x) -> ok.
Recall that DeepSec requires that the set of rewrite rules are destructor subterm convergents. In this alpha version of the tool, DeepSec does not check if the rewrite system satisfy this condition and the verification is left to the user.
Processes can be declared using the keyword
let. Note that processes can have arguments.
let processA(ca,ska,pkb) = new na; // Name restriction out(ca,aenc((na,pk(ska)),pkb)); // Output of the message aenc((na,pk(ska)),pkb) // on the channel ca in(ca,x). // Input of x on the channel ca
Conditionals can be expressed as
if u = v then P else Q or as
let pat = u in P else Q.
let processB(cb,skb,pka) = in(cb,yb); new nb; let (yna,=pka) = adec(yb,skb) in out(cb,aenc((yna,nb,pk(skb)),pka)) else out(cb,aenc(nb,pk(skb))).
let pat = u in P else Q tries to first reduce all destructor symbol in
u and second to instantiate the pattern
pat such that it becomes equal to
u. If successful,
P is executed otherwise
Q is executed. In the previous exemple, the process
out(cb,aenc((yna,nb,pk(skb)),pka)) is executed if there exists an instantiation of the variable
yna such that
yb = aenc((yna,pka),pk(skb)). Note that in the pattern
yna is a fresh variable whereas
=pka represents a term equality.
Note that processes can call other previously declared processes.
let ProcessAB = out(c,pk(ska)); out(c,pk(skb)); out(c,pk(skc)); ( processA(ca,ska,pk(skb)) | processB(cb,skb,pk(ska)) ). let ProcessCB = out(c,pk(ska)); out(c,pk(skb)); out(c,pk(skc)); ( processA(ca,skc,pk(skb)) | processB(cb,skb,pk(skc)) ).
Finally, trace equivalence queries are declared using the keyword
An input file can contain several queries. Executing the input file
To run the input file, the simplest way is to run
deepsec <name of the file>. Once the computation is completed, DeepSec generates a HTML page,
index.html, in the current directory containing a summary of the queries, the computation time and the results of each query. Additional files are generated for each query displaying the input processes, the summary of the declared name, function symbols and rewrite rules. Moreover, in case the equivalence does not hold, DeepSec also displays the corresponding attack trace.
Note that DeepSec can take several files as input. Ex:
deepsec file1 file2 file3
By default, DeepSec does not distribute the computation. To activate the distributed computation,
deepsec should be run with the option
-distributed n where
n is the number of available local cores. It is also possible to distribute computation through several computers. To do so, deepsec requires an ssh connexion between the localhost and the distant machine. The computation on distant machine must be configured with the option
-distant_workers <host> <path> <n>. The parameter
<host> is the ssh login and address (e.g my_login@my_host). The parameter
<path> should indicate the path on the distant machine the deepsec directory. Finally the parameter
<n> represents the number of cores that should be dedicated by this distant machine to the computation of the input file. As connections to distant machines are performed through ssh we recommend to configure a passwordless authentication, e.g., using ssh keys.
Note that that the option
-distant_workers should be used for each distant machine.
deepsec -distributed 20 -distant_workers login1@host1 tools/deepsec 15 -distant_workers login2@host2 deepsec 35 my_file.dps
In this command line, the first machine should be accessible with
ssh login1@host1 and the DeepSec directory should be located at
~/tools/deepsec on this machine. Similarly, the second machine should be accessible with
ssh login2@host1 and the DeepSec directory should be located at
~/deepsec. If the connexions to both machines are successful, DeepSec will distribute the computation of the file
my_file.dps between 20 local cores, 15 cores on the first machine and 35 on the second machine.
IMPORTANT: The localhost and distant machines should have exactly the same version of DeepSec (The Git hash is displayed when running
deepsec without parameters or with the option
-help) compiled with the same version of OCaml.