# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 4 Formalizing Cryptographic Protocol
### Modeling Action Models  
The changes of the language model depend on the action execution in the protocol. That is to say, the action execution results in a change of model. So, we firstly give the action model. We have given the initial model \(\mathfrak{M}\) and the action model \(Crypto_{Intr}\). Assuming set \(Ag\) be the set of agents in this protocol, we will take \(T\) (\(T\in Ag\)) as the intruder's name that performs the intruder's actions. So, in this system, \(A=Ag\cup\{In,Out\}\), and \(B=Ag\).  
We give the action model \(Crypto_{Intr}\). Intruder's actions and actions of the protocol requirement are conducted according to the intruder model and the protocol specification from the set of the actions \(\mathcal{A}\) in \(Crypto_{Intr}\).  
In the protocol, \(a\to b:m\) means that agent \(a\) sends message \(m\) to agent \(b\). We split the action into two parts: '_send_' (\(\sigma\)) \(a\to In:m\) and '_receive_' (\(\delta\)) \(Out\to b:m\). The preconditions of actions for execution are that agent \(a\) can construct \(m\) from his information set: \(Pre(\sigma)=const_{a}m\). Postcondition of the action \(\sigma\) is \(Pos_{I}(\sigma)=m\in I_{In}\). We use \(\sigma^{+}\) or \(\sigma^{-}\) to mark or unmark actions. Similarly, the precondition of action \(\delta\) is: \(Pre(\delta)=has_{Out}m\). We stipulate that the buffer can not construct any new message. Postcondition of \(\delta\) is: \(Pos_{I}=m\in I_{b}\) and a possible action marking. A specific action in \(\mathcal{A}\) is transformed into a parameterized set of the action model. We will model the intruder's actions.  
**Intruder's actions**: In the network model, we assume the intruder can eavesdrop all information from the buffer. So, the form of intruder's actions is either \(In\to T:m\) or \(T\to Out:m\). That is to say, on the one hand, the intruder can take any message from the in-buffer; on the other hand, the intruder can construct any message and put it into the out-buffer. These actions are described as parameterized actions in the action model as Table 1.  
**Epistemic relations between actions**: In the system, an agent can only distinguish the actions that he has performed. The other actions are indistinguishable for the agent. We use \(\sim_{a}\) to denote  
\begin{table}
\begin{tabular}{l l l l l l} \hline \hline
**Action** & **Direction** & **Message** & **_Pre_** & \(Pos_{I}\)** & \(Pos_{AL}\) \\ \hline take \(m\) & \(In\to T\) & \(m\) & \(has_{In}m\) & \(m\in I_{T}\) & - \\ fake \(m\) & \(T\to Out\) & \(m\) & \(const_{T}m\) & \(m\in I_{Out}\) & - \\ \hline \hline \end{tabular}
\end{table}
Table 1: Action model of the intruder.  
indistinguishable epistemic relation between actions for all agent \(a\). We will construct \(\sim_{T}\) to display indistinguishable actions for the intruder.  
**Initial Model**: In the protocol, at the initial state, details in the model \(\mathfrak{M}=(W,\{R_{a}\}_{a\in B},I,AL)\) can be described as below.  
* \(W\): a non-empty set of worlds.
* \(R_{a}\): Let \(wR_{a}v\) if and only if \(I_{(w,a)}=I_{(v,a)}(R_{a}\) is equivalence relations for \(a\) or \(a\) can not distinguish \(w\) from \(v\)).
* \(I\): \(I\) is the set of information for the agents. We say an agent's information set is always based on a certain world. So, any agent \(a\) (except the buffer) and its information set \(I\) define a world \(w\). Generally, we write it as \(I_{w,a}\). In the initial state, we stipulate the buffer is empty. Therefore, \(I_{(w,In)}=I_{(w,Out)}=\emptyset\).
* \(AL\): In the initial model, we let \(AL(w)=\emptyset\), for all \(w\in W\).  
In the following, we will analyze a specific cryptographic protocol with the formalization method on the above-mentioned.