Laboratoire Spécification et Vérification, CNRS, INRIA, Ecole Normale Supérieure de Cachan, Cachan, France
Abstract:
We consider an important family of cryptographic protocols and a class of security properties which encompasses secrecy and authentication. We show that it is always sufficient to consider a bounded number of agents b (b = 2 for secrecy properties for example): if there is an attack involving n agents, then there is an attack involving at most b agents.