Modelling cryptographic protocols by belief change operators in dynamic domains

加密协议是用于在因特网或ATM网络等敌对环境中交换信息的正式消息序列。这样的协议可以被认为具有认知目标，因为协议的成功运行旨在使参与者持有某些真实的信念（例如另一个参与者还活着，或者已经收到了某个消息）。因此，处理代理信念的认知逻辑已被用于验证加密协议。尽管这些验证方法与信念有关，但它们本质上是句法性的，因为给出了一组规则来确定代理的信念。此外，虽然理想情况下，人们希望能够处理代理不断变化的信念，但迄今为止，这种方法只能处理代理信念的细化或缩小。我们建议开发一种新的协议验证方法，其中一个明确的，声明性的行为模型及其后果与信念变化的逻辑相结合。在这种情况下，协议参与者能够收回对新信息的信念，协议参与者能够假设最合理或最可能的事件来解释新信息。因此，与以前的工作不同，我们将对代理可能具有错误信念的情况进行建模。该方法的另一个新颖之处在于，它提供了消息传递环境的显式模型，以及各种参与者的角色。

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.