Modelling cryptographic protocols by belief change operators in dynamic domains

点击翻译按钮获取中文摘要

Cryptographic protocols are formal sequences of messages that are used for exchanging information in a hostile environment such as on the internet or over an ATM network. Such protocols can be thought of as having an epistemic goal, in that a successful run of a protocol is intended to cause a participant to hold certain true beliefs (such as that another participant is alive, or has received a certain message). As such, epistemic logics, which deal with an agent's beliefs, have been employed for the verification of cryptographic protocols.Although these approaches to verification are concerned with beliefs, they are essentially syntactic, in that a set of rules is given that determines an agent's beliefs. Moreover, while ideally one would want to be able to deal with an agent's changing beliefs, such approaches to date can only deal with a refinement, or narrowing, of an agent's beliefs. We propose to develop a new approach to protocol verification, in which an explicit, declarative model of actions and their consequences is combined with a logic of belief change. 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 or possible events explaining new information. Thus, unlike previous work, we will model the case wherein an agent may have incorrect beliefs. A further novelty of the approach is that it provides an explicit model of the message-passing environment, along with the roles of the various participants.