24 September 2008, Belief Change and Information Security, Aaron Hunter

Abstract

Logics of belief have been employed for cryptographic protocol verification, because many protocols have goals that are explicitly defined in terms of the beliefs of protocol participants. For example, the goal of an authentication protocol is to convince each participant to hold certain beliefs about the identity of the other participants. It is clear that the beliefs of protocol participants change as messages are exchanged, but existing protocol logics have modeled this change with simple monotonic rules. This is a problem, because it is not possible for an agent to retract beliefs or deal with inconsistency in such a framework. However, models of rational belief change have been extensively addressed elsewhere, through the development of a formal theory of Belief Revision. In this talk, we explore the application of formal belief change operators in the analysis of security protocols. We illustrate that belief change operators can provide a more appropriate model of participant beliefs, which facilitates formal verification as well as goal discovery. We conclude by introducing an emerging application of belief change in the analysis of digitally signed documents. The talk will be self-contained, and no background in belief change will be assumed.

For more information, see http://www.cs.sfu.ca/~hunter/personal/research.html, or contact Ulle Endriss <ulle.endriss at uva.nl>.