# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 1 Introduction  
The security of cryptographic protocols is crucial in the design of the protocols as cryptographic protocols need to consider attacks from attackers. If there is any security flaw in a cryptographic protocol, the protocol can be attacked by attackers or intruders. Therefore, the security verification of cryptographic protocols is particularly important for checking whether the protocol meets security goals. To verify the security of cryptographic protocols, there are many methods. In these methods, logic-based methods play an important role. There are many works of literature (e.g., [1; 2; 3; 4; 5]) on the application of logical methods to analyze and verify cryptographic protocols. The earliest analysis method of logic is based on the Dolev-Yao model [6]. It is well known that the Dolev-Yao model opens the way for the study of formalization. Since then, a variety of cryptographic protocol analysis methods based on logic have come out. Most of the protocols analyzed by epistemic logic are authentication protocols in the existing literature. They use the method of model checking to analyze. For example, in the paper [7], the researchers propose two virtual agents to complete encryption and decryption, and construct a model checker to check the protocol. In other papers, KD45 system's belief logic is used. It needs to describe the belief logic of the protocol, and then establish reasoning rules to infer the security of the protocol. In particular, the cryptographic protocol we mentioned here refers to the protocol using classical cryptography. With the research of quantum computer, quantum cryptography is a research trend. The latest development of quantum cryptography was given in the paper [8]. This article introduced a lot about quantum key distribution (QKD). Similarly, [PERSON] and [PERSON] et al. were also doing research on quantum key distribution [9]. They illustrated how to use QKD technology to break through the limitation of low key rate and produce high key rate on a 37-core fiber. At present, the wide application of quantum technology has great challenges. Security verification of quantum cryptography protocol may be more challenging. It will be our next research content. Now, we construct an accuratedynamic epistemic logic language to describe the protocol with classical cryptography and give the action model according to the action characteristics. The action model is used to accurately describe the protocol action, and the execution process of the protocol action is the operation process of the protocol. The execution process of action is also expressed clearly and intuitively, so the whole operation process of the cryptographic protocol is completely formalized. Our verification does not need complex rules and reasoning, only through the action description table can get the results. We summarize our work as follows:  
* Applying dynamic epistemic logic, a formal language is developed to describe the cryptographic protocol. The syntax and semantics of this language are given. Cryptographic primitives and special propositions are built. * The action model is constructed to display action elements. Through update execution, the model is updated. The execution of actions results in changes between models. We model the protocol accurately. In a sense, the logic description is the logic analysis for cryptographic protocols. * With a logical language and the action model, a specific example is verified. The protocol is that a secret message is transmitted between two users who only have their own key. The goal of the protocol is that only the two users know the secret message and the outside intruder can not know the secret message after the execution of the protocol. We give the goal models. Through analysis and proof, we show that the protocol meets the intended requirements and the protocol is secure. The rest of the paper is arranged as follows. The second section displays related work about verification and analysis of the cryptographic protocol.