UKano

Porridge

Porridge

Porridge is an OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols.
It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups.

The tool Porridge, underlying techniques and experimental results are formally described in the following paper:

D. Baelde, S. Delaune and L. Hirschi. POR for Security Protocol Equivalences: Beyond Action-Determinism. Accepted at European Symposium on Research in Computer Security (ESORICS), 2018. Extended version (PDF). Conference paper (PDF).

Archive with Porridge and Deepsec source code and our case studies. Modified sources of Apte
The ESORICS'18 paper and the extended version.

Quick instructions to install and test Porridge

Build

The code builds with OCaml 4.05.0 or later. It requires the Alcotest library >=0.8.1, and ocamlfind.

You may use opam to get these requirements, using the following commands once you have opam installed and up-to-date:

$ opam switch 4.05.0
$ eval `opam config env`
$ opam install ocamlfind alcotest

Then simply run:

$ make

In more details, make targets include:

$ make lib      # build only the library
$ make test     # test it
$ make porridge # build a utility to play with the lib on predefined examples
$ make doc      # build documentation for "toplevel" modules in doc/

Install

To install/uninstall the library, run $ make install or $ make uninstall. The library will be usable with ocamlfind.

You can also use with opam:

$ opam pin add porridge .

Then $ opam install/uninstall/upgrade porridge can simply be used to install, uninstall, or upgrade the porridge library based on the latest sources.

Once the library is installed, you can install the modified version of DeepSec or Apte that leverages Porridge for reducing the search space.

Code

The src/ subdirectory contains the code. The main modules are:

LTS: our generic notion of symbolic transition system
POR: given an LTS, compute persistent sets, define the induced persistent and sleep set LTS
Trace_equiv: the symbolic LTS for trace equivalence of security protocols

See doc subdirectory, after running make doc, for more details.

We also use various utility modules, including:

Hashcons for various (interchangeable) hashconsing strategies
Memo plays a similar role for memoization

Porridge and its integration in DeepSec and Apte are developed by D. Baelde, S. Delaune and L. Hirschi.

Last update: April 11th 2018.