 |
|
 |
Back to list of 2001/02 seminars
Abstract for Seminar
| The Evolution of Protocol Security and Insecurity | ||
|---|---|---|
| Tuesday 19 February 2002 | 16:00 | Brian Spratt Room |
|
John Clark
Senior Lecturer in Critical Systems University of York |
Abstract | |
I shall deliver a two-part talk.
The Evolution of Security: Secure protocol analysis has been the major security research topic of the past decade. Comprising only a few messages, these protocols lend themselves to formal analysis by techniques such as model checking and proofs of correctness. The field has proven very popular with academia. Most work in secure protocols is about the automated analysis (and not automated design) of secure protocols.
In this talk I shall indicate how heuristic search approaches such as genetic algorithms and simulated annealing can be used to evolve protocol abstractions whose abstract execution is a proof of their own correctness. The belief logic of Burrows, Abadi and Needham is used as the specification notation. A message contains a subset of the sender's beliefs about the world. On receiving a message the receiver updates his current belief state in a way defined by the logic (the inference rules constrain the receiver to update his beliefs in an intuitively secure way). Once the senders, receivers and contents a the messages are known the protocol can be 'executed'. At the end of a protocol execution each principal involved has a set of beliefs. A protocol specification is a pre/postcondition pair of beliefs. The approach seeks to evolve protocols so that the final beliefs obtained contain the desired ones. The approach is highly unusual. Every evolved protocol achieves something and comes complete with its own proof of correctness. The issue is whether it is achieving something you want.
The Evolution of Insecurity: Some protocols concerned with identification are based on well-known NP-complete problems. This may be regarded as home ground for attacks by heuristic search and indeed people have tried this. However, all such approaches have been very direct. In this talk I shall deviate from such directness. The search process itself has a computational dynamics that can reveal more secret information than the 'answer' produced at the end of the search - it's not what you do it's the way that you do it. For a recently designed protocol over half thesecret key bits can be found within a few minutes by simply watching the search in action.
