Using Probabilistic I/O Automata to improve the analysis of cryptographic protocols

Modelling cryptographic protocols and analysing their security is a tricky business. On the one hand, valid modelling and analysis must address the concurrency aspects of asynchronous distributed systems, with potentially adversarial scheduling of events. On the other hand, realistic analysis must accommodate the fact that, in most interesting cases, it is impossible to completely prevent successful attacks against the protocol. Instead, we can only bound the success probability of attacks that use a bounded amount of computational resources, based on underlying computational hardness assumptions.