# Efficient Verification of Cryptographic Protocols with Dynamic Epistemic Logic
## 5 Verification of the Protocol
### Verification of the Protocol  
**Proposition 1**.: _For any set of message terms \(M\), and any secret message \(m\): without \(k\), if \(m\
otin\overline{M}\) then \(m\
otin\overline{m_{k}\cup M}\)._  
Proof.: From the construction rules, if an agent has \(m_{k}\) and corresponding \(k\) then he can compute \(m\). Without \(k\), if \(m\) can not be derived form \(M\), then \(m\) can not be constructed even if \(m_{k}\) is added, because of lacking a premise condition. According to this proposition, \(T\) can not compute secret message \(m\), because all messages he has from the In-buffer are encrypted data and he does not have the corresponding \(k\).  
In this system, messages in the information set for any agent are always increasing and never decreasing or deleting. So, we have:  
**Proposition 2**.: _For any message \(m\) and any agent \(a\), if agent \(a\) can construct message \(m\), then he still can construct message \(m\) after the execution of the protocol actions._  
\[\mathfrak{M}\models\mathit{const}_{a}m\rightarrow[\mathit{Crypto}_{ Intr}]\mathit{const}_{a}m\]  
**Proposition 3**.: _Target 2 is globally true in the model \(\mathfrak{M}\)._  
In the initial state, only \(S\) has the secret message \(m\) and others do not have \(m\). Of course, the intruder has \(m\) impossibly because any action is not done yet.  
Now, we prove that Target 2 is still true after the execution of the sequence of the actions.  
Proof.: We assume there exists a world \(w\) that satisfies the below case:  
\[\mathfrak{M},w\
ot\models\
eg\mathit{has}_{T}m\rightarrow[\mathit{Crypto }_{Intr}]\
eg\mathit{const}_{T}m\]  
If the above formula holds, then there exists an action sequence \(\sigma_{1},\sigma_{2},...,\sigma_{n}(\sigma_{i}\in\mathcal{A})\) such that  
\[\mathfrak{M},w\models\
eg\mathit{has}_{T}m\wedge[\mathit{Crypto}_{ Intr},\sigma_{1}]...[\mathit{Crypto}_{Intr},\sigma_{n}]\mathit{const}_{T}m\]  
From Table 3, we see that:  
\[\mathfrak{M},w\models\
eg\mathit{has}_{T}m\wedge[\mathit{Crypto}_{ Intr},\sigma_{1}]...[\mathit{Crypto}_{Intr},\delta_{3}]\
eg\mathit{const}_{T}m\]  
So, the assumption contradicts it.  
The intruder only can get the messages from the In-buffer. So, if \(m\in I_{In}\) then \(m\in I_{T}\). We list the information in the In-buffer \(\bigcup\limits_{1\leq i\leq n}I_{(w_{i},In)}=\{m_{s},m_{sr},m_{r}\}\). Therefore, all the information \(T\) has is encrypted. Without corresponding \(k\), he can not compute and get secret message \(m\). Therefore, Target 2 is satisfied.  
**Proposition 4**.: _Target 1 does not hold in the initial state. But after the running of the last action \(\delta_{3}\), Target 1 holds._  
Proof.: In the initial state, \(R\) does not have \(m\) and \(R\) only has his own key \(k_{r}\) (that is assumed in the protocol). According to Table 3, the information set of \(R\) is \(\bigcup\limits_{1\leq i\leq n}I_{(w_{i},R)}=\{m_{s},m_{sr},m_{r}\}\). Also, \(R\) has \(k_{r}\) and \(m_{r}\). According to the construction rules, \(R\) can construct \(m\), namely, \(\mathit{const}_{R}m\).  
Therefore, after the execution of all actions, we have:  
\[\mathfrak{M}\models[\sigma_{1}][take][fake][\delta_{1}][\sigma_{2}][take][fake][ \delta_{2}][\sigma_{3}][take][fake][\delta_{3}]const_{R}m\]  
which conforms to Target 1 (and everybody in the protocol knows that \(R\) has an encrypted message and corresponding key and \(R\) can construct \(m\)).  
Therefore, this protocol is secure.