Welcome to the Hermes webpage

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.


  • 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


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)