Soft Constraint Programming to Analysing Security Protocols
Giampaolo Bella, Stefano Bistarelli · 2001
Security protocols stipulate how 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. 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. We briefly describe that attack, and demonstrate the framework on a bigger, largely deployed protocol consisting of three phases, Kerberos.