[SegalaT07] Approximated Computationally Bounded Simulation Relations for Probabilistic Automata Segala, R. and Turrini, A. In 20th IEEE Computer Security Foundations Symposium (CSF), pages 140-154, IEEE Computer Society, 2007.
Downloads: pdf, bibURL: 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.