Belief Change and Cryptographic Protocol Verification

Abstract

Cryptographic protocols are structured sequences of messages that are used for
exchanging information in a hostile environment.  Many protocols have epistemic
goals: a successful run of the protocol is intended to cause a participant to hold
certain beliefs.  As such, epistemic logics have been employed for the verification
of cryptographic protocols.  Although this
approach to verification is explicitly concerned with changing
beliefs, formal belief change operators have not been incorporated in previous work.
In this paper, we introduce a new approach to protocol verification
by combining a monotonic logic with a non-monotonic belief change
operator.  In this context, a protocol participant is able to retract beliefs
in response to new information and a protocol participant is able to postulate
the most plausible event explaining new information.  We illustrate that this kind of reasoning
is particularly important when protocol participants have incorrect beliefs.