CASRUL

CASRUL is a system for automatic verification of cryptographic protocols. It translates a protocol given in common abstract syntax into a rewrite system.
This rewrite system can then be processed with a first order theorem prover for equational logic for the automatic detection of flaws.

We have experimented our system on many protocols with the prover daTac, with computing times. We have succeded in finding a new type flaw in the Denning Sacco symmetric key protocol reported here. A description of the strategy implemented in CASRUL can be found here.

CASRUL is part of the European Project AVISS, with objective to build a tool for efficient protocol analysis.

A specialised decision procedure called ATSE has also been implemented with computing times. This is a direct implementation of CASRUL search rules, with some data structure optimisations.

Contributors