Hostname: page-component-7c8c6479df-7qhmt Total loading time: 0 Render date: 2024-03-28T14:48:30.873Z Has data issue: false hasContentIssue false

Soft constraint programming to analysing security protocols

Published online by Cambridge University Press:  12 August 2004

GIAMPAOLO BELLA
Affiliation:
Dipartimento di Matematica e Informatica, Università di Catania, Viale A. Doria 6, I-95125 Catania, Italy (e-mail: giamp@dmi.unict.it)
STEFANO BISTARELLI
Affiliation:
Istituto di Informatica e Telematica, CNR, Via G. Moruzzi 1, I-56124 Pisa, Italy e-mail: stefano.bistarelli@iit.cnr.it Dipartimento di Scienze, Università “D'Annunzio”, Viale Pindaro 42, I-65127 Pescara, Italy e-mail: bista@sci.unich.it

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 (Bella and Bistarelli 2001; Bella and Bistarelli 2002), 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.

Type
Regular Papers
Copyright
© 2004 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)