Breaking security protocols as an AI planning problem

Properties like confidentiality, authentication and integrity are of increasing importance to communication protocols. Hence the development of formal methods for the verification of security protocols. This paper proposes to represent the verification of security properties as a (deductive or model-based) logical AI planning problem. The key intuition is that security attacks can be seen as plans. Rather then achieving "positive" goals a planner must exploit the structure of a security protocol and coordinate the communications steps of the agents and the network (or a potential enemy) to reach a security violation. The planning problem is formalized with a variant of dynamic logic where actions are explicit computation (such as cryptanalyzing a message) and communications steps between agents. A theory of computational properties is then coupled with a description of the particular communication protocols and an example for a key-distribution protocol is shown.