What is correctness of security protocols?

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Bella, Giampaolo en
dc.date.accessioned 2012-04-03T08:45:34Z
dc.date.available 2012-04-03T08:45:34Z
dc.date.issued 2008
dc.identifier.citation Bella, G. (2008) What is Correctness of Security Protocols? Journal of Universal Computer Science, 14, (12), pp 2083-2107 en
dc.identifier.issn 0948-695X
dc.identifier.uri http://hdl.handle.net/2086/5864
dc.description.abstract As soon as major protocol flaws were discovered empirically — a good luck that is not older than the early 1990s — this title question came up to the world. It was soon realised that some notion of formal correctness was necessary to substantiate the confidence derived from informal analyses. But protocol correctness was born in a decade when security in general was only beginning to ferment. Security protocols aim at a large variety of goals. This is partly due to the increasing domains where the protocols are finding an application, such as secure access to local area network services, secure e-mail, e-commerce, public-key registration at certification authorities and so on. Also, several interpretations are possible about each goal. Clearly, it is impossible to study protocol correctness profitably without a universal and unambiguous interpretation of its goals. What may be typical of security problems is that it is at least as important to state a detailed and appropriate model of threats that a secure system is meant to withstand. This has been a second and significant source of perhaps useless debates around many protocols. These are certain to be some of the reasons why dozens of papers appeared about one, now popular, protocol attack in just a few years of the second half of the last decade. One of the protocol designers firmly refused those ”findings” because his protocol had been conceived within a different threat model — and perhaps for different goals — from the one that the publications had been constructed upon. It seems obvious that an ant may survive under a single sheet of paper but certainly will not under a hard-back bulky book. It should be clarified what an ant and a bulky book precisely are. With particular attention to similar issues, this position paper discusses some findings of the author’s in the area of protocol formal analysis. Their significance mostly is methodical rather than specific for particular protocols. The paper then outlines the author’s favourite tool, the Inductive Method, and concludes with a few open problems. en
dc.language.iso en en
dc.subject protocol goal en
dc.subject threat model en
dc.subject protocol verification en
dc.subject inductive method en
dc.title What is correctness of security protocols? en
dc.type Article en
dc.identifier.doi http://dx.doi.org/10.3217/jucs-014-12-2083
dc.researchgroup Software Technology Research Laboratory (STRL) en
dc.ref2014.selected 1367395509_1010680226037_11_4

Files in this item

Files Size Format View

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record