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.

• Type: Conference
• Year: 2004
• Where: FOSSACS
• Authors: Ajith Ramanathan, John C. Mitchell, Andre Scedrov, Vanessa Teague
• Keywords: Applied Computing, El Gamal, El Gamal Encryption, Equational Proof System, FOSSACS 2004