# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 3 A Dynamic Epistemic Language for Cryptographic Protocols
### Semantics of the Language \(\mathcal{L}^{A,B}_{cryp}\)  
Definition 5 (Models of the language \(\mathcal{L}^{A,B}_{cryp}\)): The model is a tuple:  
\[\mathfrak{M}=(W,\{R_{a}\}_{a\in\mathbb{B}},I,AL)\]  
where \(W\) is a non-empty set of a possible world, \(R_{a}\) is binary equivalence relations on \(W\) for all \(a\in B\), \(I\) means information sets, \(I_{w,a}\) means that agent a possesses the set of information at the world \(w\), that is \(I:W\times A\rightarrow\mathcal{P}(M)\). \(AL\) denotes the action label that is \(AL:W\rightarrow\mathcal{P}(\mathcal{A})\). For \(\sigma\in\mathcal{A}\), \(tg(\sigma)\) means action \(\sigma\) in the set \(\mathcal{A}\) has been tagged. \(I\) and \(AL\) correspond to the valuation of basic propositions. If \(m\in I_{w,a}\), \(has_{a}m\) is satisfied at the world \(w\). The \(m\) is the message that agent a possesses by receiving or by some initial distribution. Message \(m\) is also constructed by the agent from messages in his information set. That is \(const_{a}m\). In the following, we cite the idea of the paper [51] and give the construction rules. Definition 6 (Construction rules in the cryptography): There are many rules determining which messages an agent can construct from his information set:  
\[\frac{m}{m_{k}}\qquad\frac{m_{k}}{m}\qquad\frac{m}{(m,m^{\prime})}\qquad\frac {(m,m^{\prime})}{m}\qquad\frac{(m,m^{\prime})}{m^{\prime}}\]_where \(m_{k}\) denotes a message \(m\) encrypted with key \(k\). \((m,m)\) denotes concatenation of two messages. In these expressions, above the line is the condition, below the line is the result. The first one says, if an agent has message \(m\) and a key \(k\) in his information set, he should be able to construct \(m_{k}\). The others are similar and will not be described._  
The satisfaction relations of basic propositions are defined as follows. **Definition 7** (Semantics of basic propositions). : _Let \(\mathfrak{M}\) be a model for \(\mathcal{L}^{A,B}_{crypt},w\in W\)._  
\(\mathfrak{M},w\models has_{a}m\) _iff_ \(m\in I_{w,a}\)__  
\(\mathfrak{M},w\models const_{a}m\) _iff_ \(m\in\overline{I_{w,a}}\)__  
\(\mathfrak{M},w\models tg(\sigma)\) _iff_ \(\sigma\in AL(w)\)__  
_The first one says if the model \(\mathfrak{M}\) satisfies agent a possesses message \(m\) in the world \(w\), if and only if (iff), \(m\) is in information set of agent \(a\) in the world \(w\). The second says agent a constructs \(m\) at \((\mathfrak{M},w)\), if and only if, \(m\) can be derived from the information set of agent \(a\) at the world \(w\). \(\overline{I_{w,a}}\) denotes that can be derived from \(I_{w,a}\). The last one illustrates that \(tg(\sigma)\) holds at \((\mathfrak{M},w)\), if and only if, \(\sigma\) is tagged at the world \(w\)._  
Having different basic propositions at the different world displays the transformation between models. This updating execution is defined as follows. **Definition 8** (Updated model). : _Let \(\mathfrak{M}\) be a model for \(\mathcal{L}^{A,B}_{crypt}\) and \(\mathfrak{A}\) be an action model, the updated model \(\mathfrak{M}\circ\mathfrak{A}=(W^{\prime},\{R^{\prime}_{a}\}_{a\in B},I^{ \prime},AL^{\prime})\) is defined by:_  
\[W^{\prime} = \{\langle w,\sigma\rangle|\mathfrak{M},w\models Pre(\sigma)\}\] \[R^{\prime}_{a} = \{(\langle w,\sigma\rangle,\langle v,\sigma^{\prime}\rangle)|wR_{ a}v\;\;\text{and}\;\;\sigma\sim_{a}\sigma^{\prime}\}\] \[I^{\prime}(\langle w,\sigma\rangle,a) = \{m|\mathfrak{M},w\models Pos_{I}(\sigma)(has_{a}m)\}\] \[AL^{\prime}(\langle w,\sigma\rangle) = \{\beta|\mathfrak{M},w\models Pos_{AL}(\sigma)(tg(\beta))\}\]  
**Definition 9** (Semantics of the language \(\mathcal{L}^{A,B}_{crypt}\)). : _Given are epistemic state \((\mathfrak{M},w)\) with \(\mathfrak{M}=(W,\{R_{a}\}_{a\in B},I,AL)\), and action model \(\mathfrak{A}=(\mathcal{A},\sim_{a\in B},Pre,Pos_{I},Pos_{AL})\).