To represent the verification of security protocol as a classical AI planning problem we need to change slightly our perspective: we need a “disruptive” planner, who wants to exploit the available actions to achieve unwanted effects and somehow deceive some of the agents. The task of the panner is then to break the systems.
In a nutshell we simply need to model security attacks as plans in a suitable formalism for reasoning about actions, communications and computations. A planning task which is interesting for its characteristics:
— the planner must combine legitimate and “illegitimate” steps of the protocol to construct an attack, somehow corrdinating the bad and good agents involved in the communication;
— “illegitimate” steps are strongly constrained: they must “look like” legitimate steps, for instance the attacker can redirect a message, or modify a message by replacing the name of the sender with her own name, but must always respect the format of the messages foreseen by the protocol;
— not all undesirable states correspond to attacks we are only interested in attacks where, according to some of the legitimate parties of the protocol, “everything seems to go smoothly”;
— among possible action we have to make explicit the computational activity of the agents, and thus we have to cope with knowledge changing actions;
— we want to describe the initial condition sparingly and let the planner figure out the rest;
— not all security violations are possible for a given protocol and thus we may fail to find a plan in that case.
If we chose a formalism based on dynamic logic which has been successfully applied to planning we can use deduction to show that a plan exists and, most important
, use the proof to generate the attack. We can also try to prove that no plan exists and hence that the particular security property represented by the negation of the planning goal is attained.
Notice that we are not bound to deductive planning. Model-generation planning may be equally well suited.
As an aside remark, computational complexity is not an issue here. At first because protocols are usually short and second and foremost because the plan construction is once-off. If we can find an attack to a protocol, the protocol will be revised or the threat model will be changed. Indeed we are not using the planner for actions but rather for verification and trading time for avoiding problems is worth the trouble.
Reusing previous plan to check a modified protocol can also be configured as a problem of re-usable planning: trying to adapt past plans to a modified description of the environment and available actions.
In the rest of the paper we give a high-level introduction to security protocols. On the techincal side we introduce a dynamic logic for modeling communication and computation. Then we explain how to transform it into a planning problem, model the general communication and computing properties and discuss possible extensions.