LySaTool

The LySatool is an automated tool for verifying security properties of protocols that use cryptography to protect network communication from tampering by malicious parties. Protocols modelled in the process calculus LySa are input to the tool. The LySatool makes a fully automated program analysis that can guarantee confidentiality and authentication properties.

Software

• Download the LySatool (version 2.02). October 6, 2006.
  Installation guide. Changes. Copyright.
• Old version (version 1.1).

Documents

• User's guide to the LySatool.
• A tutorial of encoding the Otway-Rees protocol in various scenarios. The ASCII versions of the encodings are: version A and version C.
• The paper Automated Analysis of Infinite Scenarios describes the new meta-level and its analysis, which is the main novelty of version 2. The analysis results for the examples in the paper can be found here.
• Many other relevant documents and links can be found at the LySa webpage.

Comments are much welcomed and should be sent to