Conditional automata: A tool for safe removal of negligible events

Abstract

Polynomially accurate simulations [19] are relations for Probabilistic Automata that require transitions to be matched up to negligible sets provided that computation lengths are polynomially bounded. They are proposed for verification of cryptographic protocols. In this paper we introduce a general construction on probabilistic automata, called Conditional Automata, that allows us to remove safely events that occur with negligible probability. The construction is justified in terms of polynomially accurate simulations. This, combined with the hierarchical and compositional verification style that underlies simulation relations, permits one to abstract one cryptographic component at a time in a complex system. We illustrate our construction through a simple example based on nonce generation, where we remove the event of repeated nonces. © 2010 Springer-Verlag.