Validation of Prouvé protocols using the automatic tool TA4SP

We present a new process permitting to automatically ana- lyze security protocols, specied in a very powerful language, Prouv e, describing the roles of the participants as real programs. We have built a translator from Prouv e specications to a rule-based language used as input language by several very ecien t protocol analyzers. This has permitted us to successfully validate conden tiality properties of several protocols with the ta4sp tool.