Information Security Seminar 

19/06/2009, 16:15 — 17:15 — Room P3.10, Mathematics Building
Yusuke Kawamoto, School of Information Science and Technology, University of Tokyo

Computational Soundness of Observational Equivalence without Requiring Computable Parsing

There are two main approaches to the analysis of security protocols. The first is a computational approach: a message is a bit string, an attacker is modeled as a probabilistic polynomial-time interactive Turing machine, and security properties are defined as an indistinguishability game. The analysis of protocols in this approach is based on computational complexity theory and takes account of the probability that the attacker breaks the security of cryptographic primitives. The second is a symbolic approach: a message is abstracted into a symbolic expression, an attacker is a symbolic process, and security properties, such as anonymity, can be expressed by the observational equivalence of processes. The analysis in this approach assumes ideally secure cryptographic primitives and is simple to automate. Starting with the seminal work of Abadi and Rogaway, there have been several results showing the computational soundness of the symbolic approach: security proofs in the symbolic approach imply strong security guarantees based on computational complexity theory. We extend Comon-Lundh and Cortier's recent work to show the computational soundness of the applied pi-calculus for a public-key encryption scheme and a ring signature scheme in the presence of active adversaries: the observational equivalence between two processes in the applied pi-calculus implies the computational indistinguishability between the computational executions of the two processes. Our proof for computational soundness is different from all existing studies in that it does not use a computable parsing function from bitstrings to terms. With the primitives that are considered here, it would not be a big additional hypothesis to assume such a parsing function. However, conceptually, this yields different proofs, which may allow us to obtain other soundness results such as XOR or hashing, while such proofs could not be conducted in a simulatability framework called the BPW model.