Mefisto Home | Mefisto@Venice | Participants in Venice | Publications | Documentation | Tools | Events

Tools developed in Venice:

• The BANANA tool.

  BANANA is a tool for the analysis of information leakage in Mobile Ambient specifications. It allows to compare two different control flow analyses, i.e., the one by Nielson et al. and the one by Braghin et al., run on non-trivial examples. The tool is implemented in Java; it is conceived as an applet based on AWT and thus compatible with the majority of current web browsers supporting Java.

• The CoPS tool.

  CoPS allows to efficiently verify persistent non-interference propeties. It takes as input processes of the Security Process Algebra (SPA), i.e., CCS processes whose actions are partinioned into high (confidential) level actions and low level actions. CoPS can also be used to test strong and weak bisimilarity between SPA processes. Moreover, it provides a graphical picture of the Labelled Transition System representing the semantics of the process under analysis.

• The Symbolic Security Checker.

  Symbolic Security Checker is a tool for the automatic verification of cryptographic protocols. It takes as input processes of the Security Process Algebra (SPA), i.e., CCS processes whose actions are partinioned into high (confidential) level actions and low level actions. The tool then encodes the input processes as symbolic automata, thus allowing a representation which is more efficient in terms of memory usage. The tool is implemented in C++.

• The CoSeC tool.

  The Compositional Security Checker is a semantic-based tool for automatic verification of some compositional infomation flow properties. The specifications given as inputs to CoSeC are terms of the Security Process Algebra (SPA).