Tool for checking trace equivalence for security protocols
OCaml Standard ML Makefile Shell
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
examples
src
.gitignore
COPYING
Makefile
README.md
XOR.md

README.md

Akiss

Akiss is a verification tool for checking trace equivalence of security protocols. It works in the so-called symbolic model, representing protocols by processes in the applied pi-calculus, and allowing the user to describe various security primitives by an equational theory. In order to show that two processes are trace equivalent, Akiss derives a complete set of tests for each trace of each process, using a saturation procedure that performs Horn clause resolution with selection.

A detailed description of the underlying theory is available in the following papers:

The notion of everlasting indistinguishability is introduced in

  • Myrto Arapinis, Véronique Cortier, Steve Kremer, and Mark D. Ryan. Practical Everlasting Privacy. In Proceedings of the 2nd Conference on Principles of Security and Trust (POST'13), pp. 21–40, Lecture Notes in Computer Science 7796, Springer, Rome, Italy, March 2013.

Support for XOR is introduced in

  • David Baelde, Stéphanie Delaune, Ivan Gazeau, and Steve Kremer. [Symbolic verification of privacy-type properties for security protocols with XOR] (https://hal.inria.fr/hal-01533708/document) In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), IEEE Computer Society Press, Santa Barbara, USA, August 2017.

Support for else branches is introduced in

Build

You will need OCaml; version 4.02.0 is known to work.

The support for the xor operator also requires Maude:

You shouldn't need it if you don't use the feature. See XOR.md for more information on that feature.

For parallelising the saturation process, Akiss needs the following library:

This dependency is optional; when it is not available, Akiss will run sequentially.

To build, just run make.

Statistics / tests

To run tests and collect statistics, run make stats. This will run Akiss on a selection of examples from the examples directory. For each file.api file processed, a file.stats file will be created with statistics. The Makefile will pass the AKISS_OPTIONS variable as arguments to the akiss executable, so you can for example run it with 4 jobs with the following command:

make stats AKISS_OPTIONS="-j 4"

Usage

Usage:

akiss [options] < specification-file.api
  • --verbose,-verbose: enable verbose output
  • --debug, -debug: enable debug output
  • --output-dot <file>: output statement graph to
  • -j <n>: use <n> parallel jobs (if supported)
  • --ac-compatible: use the AC-compatible toolbox even on non-AC theories (experimental, needs maude)
  • --disable-por: disables partial-order reduction (por) optimisation; without this option the por optimisation is automatically enabled when processes are action determinate
  • --help, -help: display this list of options

For example:

akiss --verbose < examples/strong-secrecy/blanchet.api

A quick overview of specification files

Specification files consist of:

  • declaration of some flags;
  • a preamble declaring used symbols and their arity, private names (public names are symbols of arity 0), channels and variables;
  • the definition of an equational theory;
  • process definitions;
  • queries.

Flags

  • set xor; : declare the infix + operator and make use of the xor machinery

Preamble

The preamble is straightforward. Each item is a comma-separated list of syntactic elements used in the file. Here is an example of preamble:

symbols pair/2, fst/1, snd/1, a/0, b/0;
channels c;
evchannels bb;
privchannels p;
var x, y, z;

There are three kinds of channels: regular, private and everlasting channels. Regular channels represent channels used during a session of a protocol. Private channels cannot be read by the adversary, and always result in silent communication. Everlasting channels represent channels whose transmitted data remains available when verifying everlasting indistinguishability.

Equational theory

The equational theory is a list of rewrite rules. Akiss will work modulo this theory. For example:

rewrite fst(pair(x, y)) -> x;
rewrite snd(pair(x, y)) -> y;

Rewrite rules can be everlasting, i.e. they are used after the interaction between the protocol and the adversary is finished when verifying everlasting indistinguishability.

evrewrite fst(pair(x, y)) -> x;
evrewrite snd(pair(x, y)) -> y;

Processes

The equational theory is followed by a list of process declarations. They respect the following grammar:

declaration ::= process_name = process;

action ::=   in(channel, variable)
           | out(channel, term)
           | [term = term]
           | [term != term]

process ::=   0 | process_name | action
            | action . process
            | let variable = term in process
            | process :: process
            | process || process
            | process ++ process
            | ( process )
            | process >> process
            | if term = term then process else process
            | if term != term then process else process

The operator precedence is: "in" < >> < :: < || < ++ < ..

Queries

Akiss can answer to a variety of queries, the main ones being:

  • [not] equivalentct? P and Q;: checks coarse-grain [in]equivalence of P and Q.
  • [not] includect? P and Q;: checks coarse-grain [in]inclusion of P and Q.
  • [not] equavalentft? P and Q;: checks fine-grain [in]equivalence of P and Q.
  • [not] includeft? P and Q;: checks fine-grain [in]inclusion of P and Q.
  • [not] fwdequivalentft? P and Q;: checks forward [in]equivalence of P and Q.
  • print_traces P;: The core of Akiss works on traces. After a process is parsed according to the high-level grammar given above, it is first expanded into a set of traces before running the core algorithm of Akiss. For examples, P1 || P2 results in all interleavings of P1 and P2. The print_traces query prints those traces.
  • variants? t;: prints the variants of term t.
  • unifiers? t1 t2;: prints equational unifiers of terms t1 and t2.
  • normalize? t;: prints the normal form of term t.

Source tree

Here is a quick guide to the organization of the source code:

  • util.ml: misc utilities
  • ast.ml, parser.mly, lexer.mll: parsing of API files
  • config.ml: detects external tools
  • term.ml: term structure and basic operations on them
  • lexmaude.mll, parsemaude.mly, maude.ml: interface with maude
  • rewriting.ml: unification and variants for non-AC theories
  • theory.ml: process first half of API file, setting up the theory and appropriate rewriting toolbox
  • base.ml: data structure for the saturation algorithm
  • horn.ml: the saturation procedure itself
  • process.ml: processes and various operations on them, including the creation of protocol-related seed statements
  • seed.ml: generation of seed statements
  • lwt_compat_pure.ml: compatibility layer for systems which lack nproc
  • main.ml: process second half of API file, create theory-related seed statements and and perform queries