Automatic Verification of Simulatability in Security Protocols

This paper investigates the problem of the automatic verification of the computational indistinguishability of systems in the simulation-based security setting, which allows proving the composable security of cryptographic protocols whose security relies on computational hardness assumptions. We use task-structured probabilistic I/O automata (task-PIOA) as our modeling framework. In this context, proofs of indistinguishability between real and ideal systems are typically divided into steps involving either proofs of perfect indistinguishability or proofs of computational indistinguishability. Our method automates the proof of perfect indistinguishability for a class of simple protocols, which is, by far, the most error-prone and time-consuming part of those security proofs. We proceed by transforming the targeted real and ideal probabilistic systems into nondeterministic ones, and check the bisimulation between the obtained systems by a partition refinement algorithm. We prove the correctness of our transformation. Our method has also been implemented in a symbolic way and we showed its usefulness by applying it to a practical protocol for oblivious transfer.