CryptoKlaim Analyser

This is a historic web page. Unfortunately, several links no longer function. They will not be updated, I apologise. However, the code can still be downloaded below.

This is the webpage for the CryptoKlaim Analyser: a tool for analysing protocols written in CryptoKlaim. CryptoKlaim is a protocol language developed by Christoffer Rosenkilde Nielsen's in his Ph.D. thesis "A Verifiable Language for Cryptographic Protocols", DTU 2008. This tool is an implementation of the language and Horn analyser described therein. The thesis can be found here. The tool can be used for verifying protocols for confidentiality and integrity.

The tool has a user-friendly command-line interface. The backend presents the results in a convenient way, and can typeset the results and the input CryptKlaim program in both ASCII and HTML; the latter is especially convenient for interpreting the results.

A comprehensive guide for the tool is included with the distribution, describing the use of the tool, interpretation of the output, the CryptoKlaim language as ASCII as well as the language extensions introduced in the tool. It does not describe CryptoKlaim for someone completely unfamiliar with it, and mostly assumes that the reader has read the protocol-modelling chapters of Nielsen's thesis.

A technical guide on the implementation of the solver is also included, with the intent of being useful for someone who wish to improve the implementation. To this end, most of the source code has also been annotated with OCamldoc comments. OCamldoc HTML-pages are pre-generated and distributed with the source code.

The tool was developed along an implementation of the Iterative Horn Solver, also described in the aforementioned Ph.D. thesis. It uses this solver for solving the Horn formulas produced by the analysis of the protocols. The homepage for that project can be found here.

Please report bugs and suggestions for improvements to "jsrn at jsrn . dk". I hope the tool will be useful for you.

Johan Sebastian Rosenkilde Nielsen

Download (version )

The tool is written in OCaml and is as such platform independent, running on any platform with an OCaml interpreter. It can be downloaded here for various platforms. Compiling the tool to native-code greatly improves speed, so this is recommended if possible. It is distributed as free software under the GPL license, version 3 or later.

The version numbering is simply the version control revision, and does not follow any release system. The changelog (version control dump) for the solver can be found here.

Byte-code (all platforms)

     Full distribution (compiled, source and documentation)

     Compiled distribution (compiled and documentation)

Source (all platforms)

     Full distribution (source and documentation)

Native-code (only linux-amd64)

     Full distribution (compiled, source and documentation)

     Compiled distribution (compiled and documentation)

Last updated at Thu Nov 27 16:51:45 CET 2014.