Validation of Prouve Protocols using the Automatic Tool TA4SP
Yohan Boichut, Nikolaï Kosmatov, Laurent Vigneron · 2006
We present a new process permitting to automatically analyze security protocols, specified in a very powerful language, Prouvé, describing the roles of the participants as real programs. We have built a translator from Prouvé specifications to a rule-based language used as input language by several very efficient protocol analyzers. This has permitted us to successfully validate confidentiality properties of several protocols with the ta4sp tool.