In the greek mythology, Hermes is the keeper of secrets and the postman
of the gods. Nowadays, Hermes is also a tool dedicated to the
verification of secrecy properties of cryptographic protocols. It has
been developped at Verimag by
Y. Bouzouzou,
L. Bozga,
C. Ene,
R. Janvier,
Y. Lakhnech,
L. Mazaré
and M. Périn.
The research around Hermes has been supported by EVA
and PROUVÉ projects.
Characteristics of Hermes
Hermes has been designed to verify secrecy properties of protocols
considering:
-
an unbounded number of sessions,
-
an unbounded size of messages,
-
an unbounded number of participants, and
-
an unbounded number of nonces.
Hermes can also be used for finite sessions to settle protocols.
The principle of Hermes
Unlike to many other tools, Hermes does not proceed by estimating the
knowledge of the intruder, but it compute a set of safe messages.
Hermes used a symbolic representation based on patterns to
approximate the infinite set of safe messages.
Papers
-
TACAS'03 - Pattern-based Abstraction for verifying Secrecy in Protocols. L. Bozga, Y. Lakhnech and M. Perin
-
CAV'03 - Hermes,a tool verifying secrecy properties of unbounded security protocols. L. Bozga, Y. Lakhnech and M. Perin
Slides
Online Hermes Demo
-
Hermes 1
( EVA Project)
-
The protocol specification is written in the
EVA language defined by D. Le Métayer and F.Jacquemard
from Trusted Logic.
-
Hermes 1 uses a front-end translator (EVA to CPL) developped at the
LSV/ENS Cachan by J. Goubault-Larrecq. It extracts and completes a
model suited for verification from an EVA specification.
-
The verification engine and its underlyning
theoretical method are developed at Verimag.
-
More information (e.g., technical reports) as well as other tools for
verifying cryptographic protocols can be found on the web page of the
EVA project.
-
Hermes 2
( PROUVÉ Project)
|
