Validating Attacks on Authentication Protocols

It is possible to show that well-known attacks on authentication protocols are flawed. This is a problem, since good protocols may thus be dismissed rather than improved and poor protocols that might continue to be used although they may contain irreparable errors. This paper describes a novel method for validating attacks on authentication protocols, based on a strategy for checking that all elements of the attack have been legally obtained. A Maude-program which implements the method, identified errors in attacks on the Wide Mouthed Frog and Yahalom authentication protocols. More generally, the paper shows that the method will find all errors in attacks that originates from incompleteness of cryptographic assumptions. The main implications is that new attacks can be effectively validated even when an exhaustive state-space analysis becomes infeasible. We expect that in the future, validation will be an obligatory part in effectively checking the soundness of any attacks on security protocols.