- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Bât. 1. 1er étage
Microsoft Research - Inria Joint Centre
Parc Orsay Université
Extending ProVerif’s Resolution Algorithm for Verifying Group Protocols
Miriam Paiola
Ecole Normale Supérieure
Many results for the automatic verification of cryptographic protocols are known for protocols with a bounded number of agents. However, for group protocols, where the number of participants is unbounded, there are few results and these results are generally limited. In this work, we present an extension of ProVerif, an automatic verifier based on an abstract interpretation of protocols by Horn clauses, to handle group protocols. In particular, our work focuses on the verification of secrecy properties, that is, proving that an attacker cannot get a secret.