# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 2 Related Work  
Since the Dolev-Yao model created a way of logical analysis for the cryptographic protocol, all kinds of logical analysis methods for cryptographic protocol have been introduced. The BAN (Burrows, Abadi and Needham) logic [1] is a pioneer. BAN logic verifies the security of cryptographic protocol by the formal method. This initiative has greatly stimulated the interest of researchers in the formal analysis of cryptographic protocols, and has become a milestone in the analysis of cryptographic protocols. The formalization of BAN logic is built on multiple types of model logic. In the paper [1], they gave a set of reasoning rules firstly based on the BAN logic. They analyzed the security of protocols by beliefs deduction. In the follow up research, many drawbacks in the BAN logic were found. So, the BAN logic is extended to GNY logic [10], VO logic [11] and MB logic [12]. BAN logic is constantly improved in application. Today, BAN logic is still used as a verification tool for security protocols or authentication protocols in radio frequency identification systems [13], Internet of things systems [14; 15], and remote authentication protocols [16].  
AT logic [17] was proposed by [PERSON] and [PERSON]. The problem of BAN logic is improved in the AT logic in terms of syntax, semantics and rules. The paper [18] and the book [19] employed SVO logic to analyze cryptographic protocols. The SVO logic has more strict definitions about the protocol logic. The protocol model based on the SVO logic has a wider range of applications.  
There still are many logics for analyzing cryptographic protocols, such as non-monotonic logic [20], time-dependent cryptographic protocol logic [21], protocol composition logic [22] and so on. In all logic analysis, there are four analysis types to find attacks in cryptographic protocols.  
Finding a new attack by inductive proof, the authors of [2] analyzed three protocols: a recursive protocol, Needham-Schroeder protocol, and Otway-Rees. [PERSON]'s attack and a new attack were discovered. Another paper [23] also analyzed two variants of Yahalom.  
The authors of [4] used rewriting calculus to display the Needham-Schroeder Public-Key protocol. With rewrite rules, they gave all actions in the protocol for all agents, including attackers. By these strategies and a set of rewrite rules, they could find attacks in the protocol.  
There have been many works of literature (e.g., [24; 25; 26; 27; 28]) that employ process calculus. Typed process calculus displays security information (e.g., [29; 30; 31; 32; 33]) by the idea of standard static-analysis. On operating cryptographic data, static-analysis has some inadequacies. So, the work in [34] improved the solution of these operations. They described the protocols and gave proof for the security of the protocols based on the typed process calculus.  
Model checking is still a widely used method to verify protocol security. The authors of [3] proposed a method that uses abstract data and deductive rules to prove the results of model checkers. [PERSON] et al. [7] developed a dynamic epistemic model checker. In the follow-up work (e.g., [35; 36; 7]), many researchers verified and analyzed security protocols with dynamic epistemic logic. The authors of [37] proposed a variant of epistemic logic methods to verify authentication protocols.  
At present, the development and application of logic go far beyond the field of philosophy [38; 39; 40]. Dynamic epistemic logic has been widely used in philosophy, sociology and computer science [41; 42; 43; 44; 45; 46; 47], and also in the verification and analysis of security protocols (see [7; 36; 37; 48]).  
Although many scholars have done a lot of work in this field, none of them is once and for all. Different protocols need different methods to analyze or verify. In this paper, dynamic epistemic logic is used to describe and analyze a specific cryptographic protocol, so as to effectively verify the security of the protocol.