µCRL toolset with POR for Branching Security Protocols


The µCRL toolset version 2.18.5 for Linux extended with POR for branching security protocols can be downloaded here.

The µCRL specifications and .tbf files of the optimistic fair exchange protocol case study can be downloaded here.

For instructions how to use the µCRL modelling language see the official website.

How to compile the µCRL toolset

Unpack the tool archive and cd to the main folder. We recommend compiling the µCRL toolset
by typing the following at the command line (as root):

1. ./configure --enable-development

2. ./make

3. ./make install

How to obtain the .tbf files from the specifications

Although the .tbf files (which are linearised versions of the µCRL specifications)
are provided in the case study package above, they can be generated
from the µCRL specifications with some additional optimisations, by typing the following
at the command line (for a given specification a.mcrl):

mcrl -stdout -regular -nocluster a.mcrl | constelm | parelm | sumelm | constelm | stategraph | constelm > a.tbf

How to use the generation algorithms in the µCRL toolset

Given a .tbf file a.tbf, type the following at the command line to run
the three different generation algorithms:

Exhaustive breadth-first generation (Gen(F))

instantiators -local a.tbf

Pruning algorithm (Gen(P))

instantiators -local -select com_recv a.tbf

Reduction algorithm (Gen(R))

instantiators -local -select1 com_recv a.tbf