Synthesis of Attack Actions Using Model Checking for the Verification of Security Protocols
Model checking cryptographic protocols have evolved to a valuable method for discovering counter-intuitive security flaws, which make possible for a hostile agent to subvert the goals of the protocol. Published works and existing security analysis tools are usually based on general intruder models that embody at least some aspects of the seminal work of Dolev-Yao, in an attempt to detect failures of secrecy. In this paper, the authors propose an alternative intruder model, which is based on a thorough analysis of how potential attacks might proceed. They introduce an intruder model that provides an open-ended base for the integration of multiple basic attack tactics.