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  or the termination is not guaranteed.
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
- Cremers, Cas J.F.; Lafourcade, Pascal; Nadeau, Philippe: Comparing state spaces in automatic security protocol analysis (2009)
- Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Approximation-based tree regular model-checking (2008)
- Janvier, Romain; Lakhnech, Yassine; Mazaré, Laurent: Computational soundness of symbolic analysis for protocols using hash functions (2007)
- Janvier, Romain; Lakhnech, Yassine; Mazaré, Laurent: Computational soundness of symbolic analysis for protocols using hash functions. (2007)
- Boichut, Y.; Héam, P.-C.; Kouchnarenko, O.: Handling algebraic properties in automatic analysis of security protocols (2006)
- Viganò, Luca: Automated security protocol analysis with the AVISPA tool. (2006)
- Zălinescu, Eugen; Cortier, Véronique; Rusinowitch, Michaël: Relating two standard notions of secrecy (2006)
- Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuellar, J.; Hankes Drielsma, P.; Heám, P.C.; Kouchnarenko, O.; Mantovani, J.; Mödersheim, S.; von Oheimb, D.; Rusinowitch, M.; Santiago, J.; Turuani, M.; Viganò, L.; Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications (2005)
- Cortier, Véronique; Warinschi, Bogdan: Computationally sound, automated proofs for security protocols (2005)
- Janvier, Romain; Lakhnech, Yassine; Mazaré, Laurent: Completing the picture: Soundness of formal encryption in the presence of active adversaries (2005)