# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 3 A Dynamic Epistemic Language for Cryptographic Protocols
### Syntax of the Language \(\mathcal{L}_{\mathit{crypt}}^{A,B}\)  
Before giving the syntax of the language, we define some basic concepts about this language. **Definition 1** (Message). : \(M\) _is taken as the set of messages._  
_Message_ \(m\) _in the protocol as logic term is defined by:_  
\[m::=\ n\mid k\mid\{m\}_{k}\mid(m,m^{\prime})\]  
_where_ \(n\) _is a nonce or encoding of a message in ASCII; generally,_ \(n\) _denotes a plain message. Also,_ \(k\) _is crypto-key._ \(\{m\}_{k}\) _is the encryption of_ \(m\) _with key_ \(k\) _(ciphertext message) and_ \((m,m^{\prime})\) _intuitively, represents concatenating of_ \(m\) _and_ \(m^{\prime}\)_._  
**Definition 2** (Propositions). : _In this system, the set \(\Phi_{\mathit{crypt}}^{A}\) as the set of basic propositions \(p\) that is defined by:_  
\[p::=\mathit{has}_{a}m\mid\mathit{const}_{a}m\mid\mathit{tg}(\sigma)\]  
_where \(a\in A\), \(m\in M\) and \(\sigma\in\mathcal{A}\). \(\mathit{has}_{a}m\) means agent a possesses message \(m\) (the message is received by agent a or initial distribution). \(\mathit{const}_{a}m\) means agent a can construct \(m\) from the messages he possesses. \(\mathit{tg}(\sigma)\) denotes action \(\sigma\) is tagged. Let \(\Phi_{I}\), \(\Phi_{\bar{I}^{\prime}_{\sigma}}\), \(\Phi_{tg}\), be subsets of \(\Phi_{\mathit{crypt}}^{A}\) that contain the above three propositions, respectively. Then, we will define action models._We will give a definition of about action models according to the idea of the paper [49; 50]. The condition of an action execution is called _precondition_. Without corresponding preconditions, the action can not be executed. In this system, all preconditions belong to \(\Phi^{A}_{cyp}\), which is a part of the language \(\mathcal{L}^{A,B}_{cryp}\). Facts that will hold after the execution of an action are called _postcondition_. Postcondition displays the changing of basic facts after running the action. Postcondition is divided into two parts: the one is \(Pos_{1}\) that shows changes for the information sets including messages that are sent by the agents, another is \(Pos_{AL}\), which illustrates the changes for action labels that show the actions have been performed by the agents. Definition 3 (Action model): Based on the logical language \(\mathcal{L}^{A,B}_{cryp}\), an action model \(\mathfrak{A}\) is a structure: \(\mathfrak{A}=(\mathcal{A},\sim_{a\in\mathbb{B}},Pre,Pos_{1},Pos_{AL})\), where \(\mathcal{A}\) is non-empty and finite set of actions, \(\sim_{a}\) is an equivalence relation (reflexive, symmetric and transitive) on \(\mathcal{A}\) for all \(a\in B\). \(Pre:\mathcal{A}\rightarrow\Phi^{A}_{cryp}\) assigns a propositional precondition for every action. We employ the idea of paper [49] to deal with the postcondition. \(\Phi\) is a set of propositions for the language \(\mathcal{L}^{A,B}_{cryp}\). For the sake of simplicity of description, we will use a substitution in this model structure. Function \(\Phi\rightarrow\mathcal{L}\) is a substitution for \(\mathcal{L}\). It maps basic propositions of the language to their variant. The \(\mathit{SUB}(\mathcal{L})\) is taken as a set of substitutions from \(\Phi\) to \(\mathcal{L}\). So, \(Pos_{1}:\mathcal{A}\rightarrow\mathit{SUB}(\mathcal{L}^{A,B}_{cryp})\) gives a substitution for \(\mathcal{L}\) that has property \(Pos_{1}(\sigma)(p)\in\Phi_{1}\cup\{\top,\bot\}\) for all \(p\in\Phi_{1}\) and \(\sigma\in\mathcal{A}\). \(Pos_{AL}:\mathcal{A}\rightarrow\mathit{SUB}(\mathcal{L}^{A,B}_{cryp})\) gives a substitution for \(\mathcal{L}\), which has the property that \(Pos_{AL}(\sigma)(p)\in\Phi_{AL}\cup\{\top,\bot\}\) for all \(p\in\Phi_{AL}\) and \(\sigma\in\mathcal{A}\). We replace 'has\({}_{a}\)m' with '\(m\in I_{a}\)' for the substitution mapping to \(\top\). Meanwhile, the message \(m\) is added to the information set of agent a after the execution of the action.