Anonymity Model Generation

This set of scripts generate PRISM models for the Dining Cryptographers and Crowds protocols. The scripts can also use PRISM to calculate the matrix of the protocol, compute its capacity and plot it as a function of the protocol parameters. More information about these experiments can be found in the paper:

K. Chatzikokolakis, C. Palamidessi, P. Panangaden.
Anonymity Protocols as Noisy Channels.
Information and Computation, 206: 378-401, 2008. pdf

Dining Cryptographers

The scripts can be found in the 'dc' directory. The main script is genmodel.pl, which generates the PRISM model for the DC protocol with an arbitrary connection graph.

To run the tool type

  perl genmodel.pl --file=filename [--fixorder]

Arguments

  --file=filename
    Based on this parameter, the script will create two files,
    filename.nm (containing the model) and filename.pctl (containing the
    PCTL formulas to check)

  --fixorder
    If this is given then all the non-determinism of the protocol will be removed and
    a fixed order of coin tosses/announceents/etc will be used. This increases the
    model-checking performance.

The connection graph can be changed by modifying the $adj variable in the beginning of the genmodel.pl file. This variable contains the adjacency matrix of the graph. The methods clique(n), cycle(n) and chain(n) are provided to easily create standard graphs, for example

  my $adj = clique(4);

will use a clique of 4 cryptographers.

If PRISM and gnuplot are installed, then the 'execute' script can automate the whole model-checking process by simply calling

  ./execute

The execute script will

call genmodel.pl and store the model in the 'models' directory.
call PRISM for various values of the probability of heads and store the results in the 'prismoutput' directory
call parsedata.pl which parses the PRISM output, computes the capacity of the matrix and stores the results in the 'final' directory.
call gnuplot to plot the capacity as a function of the probability of heads.

Crowds

The scripts can be found in the 'crowds' directory. The main script is genmodel.pl, which generates the PRISM model for the Crowds protocol with an arbitrary number of honest and corrupted users.

To run the tool type

  perl genmodel.pl --file=filename [--users=n] [--honest=m] [--one-row] [--two-cols]

Arguments

  --file=filename
    Based on this parameter, the script will create two files,
    filename.nm (containing the model) and filename.pctl (containing the
    PCTL formulas to check)

  --users=n
    The total number of crowds users

  --honest=n
    The number of honest users (must be <= the total number of users)

  --one-row
    Compute only one row of the matrix (the rest should be computed based on the
    symmetry). This does not change the model, only the PCTL formulas.

  --two-cols
    Compute only two columns of the matrix (the rest should be computed based on the
    symmetry). This does not change the model, only the PCTL formulas.

If PRISM and gnuplot are installed, then the 'execute' script can automate the whole model-checking process by simply calling

 ./execute n m

The execute script will

call genmodel.pl with --users=n --honest=m and store the model in the 'models' directory.
call PRISM for various values of the probability of forwarding (a parameter of the crowds protocol) and store the results in the 'prismoutput' directory
call parsedata.pl which parses the PRISM output, computes the capacity of the matrix and stores the results in the 'final' directory.
call gnuplot to plot the capacity as a function of the probability of forwarding.