Software

MMCsp, a compiler for the π-calculus

MMCsp is a compiler from a simple probabilistic π-calculus to PRISM models. It is built on XSB, a tabled logic programming system, and generates the symbolic semantic representation of a probabilistic pi-calculus term in text. A separate Java program then translates this semantic representation into a probabilistic model for PRISM.

The tool was developed by Peng Wu during his postdoc period in Comète, in the context of the collaboration with PRISM (Oxford University Computing Laboratory) sponsored by the INRIA/ARC Project ProNobis.

More information and code download




Tools for computing the leakage of information

The following software was developed by Konstantinos Chatzikokolakis, in the context of his PhD Thesis in Comète.
  • PRISM model generator: generates PRISM models for the Dining Cryptographers and Crowds protocols. It can also use PRISM to calculate the capacity of the corresponding channels. More information can be found in this paper.
    README file width instructions. Download.
  • Corner points: calculate the set of corner points of a channel. The corner points can be used to compute the maximum probability of error and to improve the Hellman-Raviv and Santhi-Vardy bounds. More information can be found in this paper.
    README file width instructions. Download.
Requirements: These scripts require Perl to run and have been tested in Linux. The GUI of the corners tool also requires the Perl/TK library. Finally some parts of the model generator tool require PRISM and gnuplot to be installed.