A Logic for Modeling the Dynamics of Beliefs in Cryptographic Protocols
Yan Zhang, Vijay Varadharajan · 2001
We present a logic of modeling the dynamics of beliefs in cryptographic protocols. Differently from previous proposals, our logic is situation based in which a protocol is viewed as a finite sequence of actions performed by various principals at different situations, and each action is a primitive term in the language. Therefore, it becomes possible to model the dynamic change of each principal's beliefs at each step of the protocol within the logic system. Our logic has a precise semantics and is sound with respect to the underlying axiomatic system. We also demonstrate the application of our logic through a specific protocol analysis. Keywords: belief, action and situation, logic and information security, authentication 1 Introduction Since BAN logic was proposed in 1989 [4], it quickly became the most widely discussed formal method used in the analysis of authentication protocols. It has been also noted that the original BAN logic is purely syntax-based, that is, there was...