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 article proposes to represent the verification of security properties as a 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 to reach a security voilation.
The planning problem is formalized with a variant of dynamic logic where actions are explicit computation and communications steps beteen agents. A theory of computational properties is then coupled with a description of the particular communicaton protocols and and example for a key-distribution procol is shown.
The development and formal verification of security protocols is one of the key requirement for mordern distributed systems which face the need of secure communication over an insecure network.
The key idea is to rely on cryptographic primitives to guarantee security properties viz. confidentiality, integrity or authentication.
Yet the presence of well designed cryptographic primitives is far from guaranteeing such security properties. On the contrary, most “securer” systems are not broken by cryptographic attacks, but rather by exploiting operational blunders and logical errors in the protocol design. The subtlety of logical faults may even be such that a protocol may become a standard before being proved badly broken.
Logical errors can be prevented by formal verification and a number of techniques have been developed for the logical analysis of secuactrity protocols. Formal systems abstract away the cryptographic details and develop a theory of actions where some messages can be “opened” by an agent only if she has the corresponding key.
For a formal analysis one can use logics of knowledge and belief in the same spirit of the works of Halpern et al for high-level reasoning about communication protocols. After the seminal paper on the BAN logic those logics have become a large family, e.g. At the other end of the spectrum, researches have described protocols as traces of atomic actions, modeling explicitly the properties low-level of the network. The finite states approach the process algebra CSP and model checking or on states enumeration methods can be used to find attacks whereas the approach based on induction can be used to prove properties such as secrecy and authenticity.
At this stage one may start wondering: this is surely interesting but…what formal verification has to do with planning?
Undoubtedly the use of logic and theorem proving techniques for reasoning about action is a backbone of deductive planning ad the use of proof tactcs borrowed from interactive teorem provers is the basis for both tactical planning and the verification of security properties.
The similarity is tighter for verification systems based on traces: they have a sophisticated modeling of the actions available to the legitimate participants, of the computing power of a potential enemy and of his abilities to tamper legitimate messages. This is just reasoning about action in disguise.
Yet one may argue that deductive planning and formal verification share the same tools but have different objectives. It is so because we are used to think that in a planning problem we accomplish something “good”: from stacking blocks on a table to moving a mechanical arm, from avoiding collisions between a moving robot and other objects, to complex scheduling of satellites. The second point is that we often assume that multiagent planning is cooperative.