How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones.

Hubert Comon-Lundh & VéRonique Cortier
Security protocols are short programs that aim at securing communication over a public network. Their design is known to be error-prone with flaws found years later. That is why they deserve a careful security analysis, with rigorous proofs. Two main lines of research have been (independently) developed to analyse the security of protocols. On the one hand, formal methods provide with symbolic models and often automatic proofs. On the other hand, cryptographic models propose a...