Probabilistic bisimulation and equivalence for security analysis of network protocols

Abstract

Using a probabilistic polynomial-time process calculus designed for specifying security properties as observational equivalences, we develop a form of bisimulation that justifies an equational proof system. This proof system is sufficiently powerful to derive the semantic security of El Gamal encryption from the Decision Diffie-Hellman (DDH) assumption. The proof system can also derive the converse: if El Gamal is secure, then DDH holds. While these are not new cryptographic results, these example proofs show the power of probabilistic bisimulation and equational reasoning for protocol security. © Springer-Verlag 2004.