Approximated Computationally Bounded Simulation Relations for Probabilistic Automata

Appears: Proceedings of the 20th IEEE Computer Security Foundations Symposium, Venice, Italy, pages 140-156, July 2007.

Abstract: We study simulation relations for Probabilistic Automata that require transitions to be matched up to negligible sets provided that computation lengths are polynomially bounded. These relations are meant to provide rigorous grounds to parts of correctness proofs for cryptographic protocols that are usually carried out by semi-formal arguments. We illustrate our ideas by recasting a correctness proof of Bellare and Rogaway based on the notion of matching conversation.

Download the paper from the publisher.

Download an author-created copy of the paper.