Basser Seminar Series
The Shadow Knows: Security, privacy... and refinement
Professor Carroll Morgan
Australian Professorial Fellow
School of Computer Science and Engineering
University of New South Wales
Friday 11 August 2006, 12-1 pm NOTE: Different day and time
School of IT Building, Lecture Theatre 123, Level 1
Separating sequential-program state into `visible-' and `hidden' parts facilitates reasoning about knowledge, security and privacy: applications include zero-knowledge protocols, and security contexts with hidden `high-security' state and visible `low-security' state. A rigorous definition of how specifications relate to implementations, as part of that reasoning, must ensure that implementations reveal no more than their specifications: they must, in effect, preserve ignorance.
We propose just such a definition a relation of ignorance- preserving refinement between specifications and implementations of sequential programs. Its purpose is to enable a development-by- refinement methodology for applications like those above.
Since preserving ignorance is an extra obligation, the proposed refinement relation restricts (rather than extends) the usual. We suggest general principles for restriction, and we give specific examples of them.
The talk will use either the "Dining Cryptographers" or the the "Oblivious Transfer" protocols as a running example.
Carroll Morgan graduated from UNSW (BSc) and Basser (PhD), after which he spent almost 20 years at Oxford University in the UK; he returned to UNSW in 2000. The general theme of his research has been Formal Methods, that is (broadly interpreted) the idea that a rigorous mathematical meaning for computer programs can and should be used to help ensure that those programs do what their users want, and expect.
He is the author of the research monographs "Programming from Specifications" (Prentice Hall 1990, 1994) and (with Annabelle McIver) "Abstraction, Refinement and Proof for Probabilistic Systems" (Springer, 2005).
He has only recently begun looking at security and related issues.