The Securify tool belongs to the RNTL EVA project.
It aims at verifying secrecy for cryptographic protocols considering:
an unbounded number of sessions
an unbounded size of messages
an unbounded number of participants
an unbounded number of nonces
Principle
Securify verifies that none of the protocol's rules compromises a secret. Three tests are performed for every rule and every part of a sent message:
either this part is a fresh generated nonce thus it cannot compromise any secret,
or this part was already sent on the network, encrypted with at least the same set of keys,
or this part is a secret but is encrypted with a protected key.
When none of these tests succeed, a backward search is done in order to obtain more information about the messages already sent on the network and the three tests are applied again.
A more complete information about the underlying theory may be found
here.
More information (e.g., technical reports) as well as other tools for verifying
cryptographic protocols can be found on the web page of the
RNTL EVA project.
Input
The Securify input is a protocol specification written in the
EVA language defined by D. Le Métayer
and F.Jacquemard from Trusted Logic. This input is translated in an other model (EVA to
CPL),
more suitable for verification, by a front-end translator developped at
the LSV/ENS Cachan by J. Goubault-Larrecq.
Answer to the following question : does the protocol
satisfy its requirements?
Computation time.
In addition, it produces either a proof or a proof attempt of the protocol correctness.
When the proof of the correctness fails, the proof attempt
may help to understand why the proof failed and to construct an attack.
This is the case for the Needham-Schroeder protocol given below.
Sources
You may use Securify on-line below. But the on-line version has a limited computation time and memory.
To use Securify without limitations, you may install it by downloading the
Securify archive.
The new version, which allows to verify more protocols like the Yahalom protocol but which is slower, can also be downloaded.
Note that Securify needs the installation of the EVA Translator. It may be obtained by decompressing the
EVA archive, or have a peek at the
source directory
(all files precompiled for Linux, glibc).
This uses C, OCaml, and the
HimML program (not very easy to install...).