Deciding the Correctness of Attacks on Authentication Protocols

Abstract

A new tool for automated validation of attacks on authentication protocols has been used to find several errors and ambiguities in the list of attacks described in the well known report by Clark and Jacob. In this paper the errors are presented and classified. Corrected descriptions of the incorrect attacks are given for the attacks that can be easily repaired. The underlying method for finding errors in attacks is presented, including a formal language for attack specification, a validation algorithm, and a framework for executing attacks. At the end of the paper, the connection between validation and simulation is settled: Every attack specification that can be successfully executed is valid.