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.