Soft Constraint Programming to Analysing Security Protocols

TL;DR

This paper introduces a soft constraint-based formal framework for analyzing security protocols, allowing for varying security levels of confidentiality and authentication, and demonstrates its effectiveness through analysis of Needham-Schroeder and Kerberos protocols.

Contribution

It develops a novel soft constraint formalism for security goals, enabling nuanced analysis of protocols with different security levels, and applies it to discover new attack insights.

Findings

Discovered a new attack on Needham-Schroeder protocol.

Validated the framework on the Kerberos protocol.

Showed the framework's suitability for mechanized protocol analysis.

Abstract

Security protocols stipulate how the remote principals of a computer network should interact in order to obtain specific security goals. The crucial goals of confidentiality and authentication may be achieved in various forms, each of different strength. Using soft (rather than crisp) constraints, we develop a uniform formal notion for the two goals. They are no longer formalised as mere yes/no properties as in the existing literature, but gain an extra parameter, the security level. For example, different messages can enjoy different levels of confidentiality, or a principal can achieve different levels of authentication with different principals. The goals are formalised within a general framework for protocol analysis that is amenable to mechanisation by model checking. Following the application of the framework to analysing the asymmetric Needham-Schroeder protocol, we have recently discovered a new attack on that protocol as a form of retaliation by principals who have been attacked previously. Having commented on that attack, we then demonstrate the framework on a bigger, largely deployed protocol consisting of three phases, Kerberos.