Cryptographic protocols have so far been analyzed for the most part by means of testing (which does not yield proofs of secrecy) and theorem proving (costly). We propose a new approach, based on the abstract domain of regular tree languages. While the abstraction we use seems fine-grained enough to be able to certify some protocols, there are still complexity issues to be solved. Both the formal semantics and implementation issues are discussed in the paper.

• Monniaux_SAS99.pdf
• Monniaux_SAS99.ps