Abstracting Cryptographic Protocols with Tree Automata

ing Cryptographic Protocols with Tree Automata David Monniaux http://www.di.ens.fr/%7Fmonniaux, Laboratoire d’Informatique, ´Ecole Normale Sup´erieure, 45 rue d’Ulm , 75230 PARIS c´edex 5, FRANCE 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 a new approach, based on abstract interpretation and using regular tree s. The abstraction we use seems fine-grained enough to be able to certify tocols. Both the concrete and abstract semantics of the protocol description language and implementation issues are discussed in the paper.

• Type: Conference
• Year: 1999
• Where: SAS
• Authors: David Monniaux
• Keywords: Automata David Monniaux, Cryptographic Protocols, Formal Methods, FRANCE Cryptographic Protocols, SAS 1999