K. Chatzikokolakis, C. Palamidessi, P. Panangaden.

Anonymity Protocols as Noisy Channels.

Information and Computation, 206: 378-401, 2008. pdf

To run the tool type

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

--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

./executeThe 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.

To run the tool type

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

--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 mThe 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.