Security protocols verification in abductive logic programming: a case study

In this paper we present by a case study an approach to the verification of security protocols based on Abductive Logic Programming. We start from the perspective of open multi-agent systems, where the internal architecture of the individual system's components may not be completely specified, but it is important to infer and prove properties about the overall system behaviour. We take a formal approach based on Computational Logic, to address verification at two orthogonal levels: `static' verification of protocol properties (which can guarantee, at design time, that some properties are a logical consequence of the protocol), and `dynamic' verification of compliance of agent communication (which checks, at runtime, that the agents do actually follow the protocol). We adopt as a running example the well-known Needham-Schroeder protocol. We first show how the protocol can be specified in our previously developed SOCS-SI framework, and then demonstrate the two types of verification.