A logic programming based framework for security protocol verification

Security protocol analysis has been a major research topic in information security and recognised to be a notoriously hard problem. In this paper, we take the advantage of answer set programming technology to develop an effective framework to verify security protocols carrying claimed security proof under adversary models on computational complexity theory. In our approach, a security protocol, adversary actions and attacks can be formally specified within a unified logic program. Then the verification is performed in an automatic manner by computing the stable models of the underlying logic program. We use Boyd-González Nieto conference key agreement protocol as our case study protocol to demonstrate the effectiveness and efficiency of our approach.