# Towards a Provably Secure Authentication Protocol for Fog-Driven IoT-Based Systems
## 4 Security Analysis
### Formal Security Analysis
\(Send(U_{k}^{i},Message_{4})\): After getting this send query, it is supposed that \(\Pi_{U_{k}}^{i}\) is in an expecting state, \(C\) breaks \(Message_{4}\) into \(\{N_{1},Q_{k},auth_{csp1}\}\) which verifies \(auth_{csp_{1}}^{\prime}\stackrel{{? }}{{=}}h(ID_{k}\|ID_{csp}\|X_{k} \|\mathcal{SK}_{k-f-csp}\|r_{4}\|r_{7})\). If this condition does not hold then \(C\) rejects \(\mathcal{A}_{att}^{\prime}\)s query and returns nothing. Otherwise, \(C\) calculatesand the instance of the client is accepted and terminated. Furthermore, \(\{\mathit{Message}_{1},\mathit{Message}_{2},\mathit{Message}_{3},\mathit{Message}_{4}\}\) are added to list. **Corrupt query**: In order to obtain the long term key of user, an adversary initiates this query. Upon receiving corrupt \((C,DB)\), the information stored in the database protected with secret key \(x\) is returned. **Execute \(\mathbf{(\mathcal{U}_{k}^{i},\mathit{FN}_{f}^{j},\mathcal{CSP}^{k})}\)**: On this query, the execution process of proposed protocol is simulated by \(C\) after issuing the following \(\mathit{Send}\) queries. \[\mathit{Send}\ (\mathcal{U}_{k}^{i}\ (\mathit{FN}_{f},\mathit{START}))\] \[\mathit{Send}(\mathit{FN}_{f}^{j},\mathit{Message}_{1})\] \[\mathit{Send}(\mathit{CSP}^{k},\mathit{Message}_{2})\] \[\mathit{Send}(\mathit{FN}_{f}^{j},\mathit{Message}_{3})\]  
and \(C\) returns \(\{\mathit{Message}_{1},\mathit{Message}_{2},\mathit{Message}_{3}, \mathit{Message}_{4}\}\) to \(\mathcal{A}_{att}\). **Reveal \(\Pi_{p}^{a}\)**: On receiving this query, \(C\) responds with a session key if instance \(\Pi_{l}^{a}\) is accepted; otherwise, it returns \(\bot\). **Test query**: On receiving the test query \((\mathcal{U}_{k}^{i})\), \(C\) chooses \(\tau\epsilon\{0,1\}\). If \(\tau=1\), then \(C\) gives back the true session key; otherwise, it return a the random value of similar size. The above said proof is compared on sequence games \(Gm_{0},Gm_{1},Gm_{2},Gm_{3},Gm_{4},Gm_{5}\). Let \(S_{a}\) be the event that \(\mathcal{A}_{att}\) outputs the correct \(\tau\) in game \(Gm_{a}\) (a = 0,1,2,3,4). **Game \(Gm_{0}\)**: \(Gm_{0}\) is the actual attacking game. Just like a real player, \(C\) simulates the oracle queries in this game. The chances of success in this game are quite equal to the probability that \(\mathcal{A}_{att}\) succeeds in attacking the proposed protocol and obtains the following:  
\[\epsilon=|2P_{r}[S_{0}]-1| \tag{2}\]  
**Game \(Gm_{1}\)**: This game is identical to \(Gm_{0}\). The difference is that \(C\) maintains a list of values \(L_{0}-L_{5}\). \(C\) searches the related list when the hash oracle is queried. If there exists any entry, then the same value is returned; otherwise, \(C\) returns the random value and inserts it into corresponding list \(L_{i}\). It is visible and concluded here from the properties of oracle that \(Gm_{1}\) is indistinguishable from \(Gm_{0}\). Therefore:  
\[P_{r}[S_{1}]=P_{r}[S_{0}] \tag{3}\]  
**Game \(Gm_{2}\)**: This game is identical to \(Gm_{1}\). The difference is that in this game, the simulation of all queries will be terminated only if the following two events occur:  
* **Event (\(E_{A}\))**: Collision on the result hash queries. * **Event (\(E_{B}\))**: Collision on the copy of all messages (\(\mathit{Message}_{1}\), \(\mathit{Message}_{2}\), \(\mathit{Message}_{3}\), \(\mathit{Message}_{4}\)). As per the the definition of birthday paradox: \[P_{r}[E_{a}]\leq\Sigma_{a=0}^{a=4}\frac{q_{kn}^{2}}{2p}\] (4) Since a,b,c are randomly chosen, the probability of \(E_{B}\) happening is \(P_{r}[E_{b}]\leq\frac{(q_{sn}-q_{ex})^{2}}{2p}\), where \(q_{sn}\) and \(q_{ex}\) are upper bound of the \(\mathit{Send}\) and \(\mathit{Execute}\) queries, respectively. Therefore, we have: \[|P_{r}[S_{2}]-P_{r}[S_{1}]|\leq(\Sigma_{a=0}^{a=4}q_{kn}^{2}+(q_{sn}+q_{ex})^{ 2}|(2p))\] (5)  
**Game \(Gm_{3}\)**: In this game, the send query is modified. \(C\) picks an instance \((\mathcal{U}_{k}^{i},\mathit{FN}_{f}^{j},\mathcal{CSP}^{k})\) and answers \(\mathcal{A}_{att}^{\prime}\mathit{Send}\) queries as follows:  
1.