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
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:
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.
- 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.
A more complete information about the underlying theory may be found
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.
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
more suitable for verification, by a front-end translator developped at
the LSV/ENS Cachan by J. Goubault-Larrecq.
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.
- Translation of the protocol in the
- Answer to the following question : does the protocol
satisfy its requirements?
- Computation time.
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
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
(all files precompiled for Linux, glibc).
This uses C, OCaml, and the
HimML program (not very easy to install...).
EVA tools: Securify