Approximated Computationally Bounded Simulation Relations for Probabilistic Automata
Roberto Segala, Andrea Turrini · Proceedings - Computer Security Foundations Workshop/Proceedings · 2007
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.