HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. Cryptography is not sufficient for implementing secure exchange of secrets or authentification. Logical flaws in the protocol design may lead to incorrect behavior even under the idealized assumption of perfect cryptography. Most of protocol verification tools are model-checking tools for bounded number of sessions, bounded number of participants and in many case also a bounded size of messages [11,8,5,10]. In general, they are applied to discover flaws in cryptographic protocols. On the contrary, tools based on induction and theorem proving provide a general proof strategy [9,4], but they are either not automatic with exception of [4] or the termination is not guaranteed.