Justifying Finite Resources for Adversaries in Automated Analysis of Authentication Protocols

Exhaustive state-space exploration is a powerful approach to automated verification of authentication and key establishment protocols. However, correctness of such protocols is typically expressed as properties (requirements) that must hold even in systems in which there are an unbounded number of (potentially concurrent) runs of the protocol, and in which an adversary can perform an unbounded number of decryptions while eavesdropping and an unbounded number of encryptions (and other operations) while fabricating messages. Therefore, reduction theorems are needed, which show that if the required properties hold in a system with certain finite bounds on these parameters, then the properties hold in the unbounded system as well. We prove reductions that bound the number of operations performed by the adversary; one of these reductions presupposes a bound on the number of runs of the protocol. We also sketch an approach to establishing the latter bound. 1 Introduction Exhaustive state-s..