## 6 Security Analysis
### Formal Proof Under RoR Model  
We performed a formal analysis based on the \"Real-or-Random (RoR) model\" [17] to validate a security of the session key. The queries specified in the RoR model are \(Execute\), \(CorruptMD\), \(Send\), and \(Test\)[47]. An adversary \(\mathcal{A}\) can utilize these queries to attempt various attacks. Detailed descriptions of each query are provided below, where \(\mathcal{P}_{U}^{t_{1}}\), \(\mathcal{P}_{CS}^{t_{2}}\), and \(\mathcal{P}_{S}^{t_{3}}\) denote the users, central server, and sensors in the proposed scheme, respectively. * \(Execute(\mathcal{P}_{U}^{t_{1}},\mathcal{P}_{CS}^{t_{2}},\mathcal{P}_{S}^{t_{3}})\): This query corresponds to a passive attack where \(\mathcal{A}\) eaves-drops on messages sent via a public channel between \(\mathcal{P}_{U}^{t_{1}}\), \(\mathcal{P}_{CS}^{t_{2}}\), and \(\mathcal{P}_{S}^{t_{3}}\). * \(CorruptMD(\mathcal{P}_{U}^{t_{1}})\): This query presents stolen mobile device attacks. \(\mathcal{A}\) can retrieve the confidential values stored in a user's mobile device. * \(Send(\mathcal{P}^{t},M)\): This query corresponds to an active attack in which adversary \(\mathcal{A}\) transmits a message \(M\) to \(\mathcal{P}^{t}\) and accepts the corresponding response. * \(Test(\mathcal{P}^{t})\): This query determines whether a session key is real or random. Before the game begins, \(flawA\) flips a fair coin. If \(c=1\), the returned key is the valid session key,and if \(c=0\), it is a random string. Otherwise, if the result is \(null\), \(\mathcal{A}\) cannot distinguish the session key. **Theorem 1**. : _Consider the case where \(\mathcal{A}\) attempts to compute a session key established in the proposed scheme within polynomial time. Moreover, \(Adv_{\mathcal{A}}\) denotes the probability that \(\mathcal{A}\) will obtain the session key. Therefore, the following equation can be derived:_  
\[Adv_{\mathcal{A}}\leq\frac{q_{h}^{2}}{|Hash|}+\frac{q_{p}^{2}}{|PUF|}+2\{C^{ \prime}\cdot q_{send}^{s^{\prime}}\},\]  
_where \(q_{h}\), \(q_{p}\), and \(q_{send}\) denote the number of hash, PUF, and send queries, respectively. The terms \(|Hash|\) and \(|PUF|\) represent the output space of the hash function and PUF. In addition, \(C^{\prime}\) denotes [PERSON]'s parameter [48]._  
Proof. : To validate the semantic security of the session key, we conduct a game sequence \(G_{i}\) (\(i=0,1,2,3\)). Furthermore, \(\Pr[Succ_{GMi}]\) represents the probability that \(\mathcal{A}\) successfully guesses a bit \(c\) in game \(G_{i}\). \(Game_{0}\): In this game, \(\mathcal{A}\) performs a real attack on the proposed scheme. \(\mathcal{A}\) must randomly select a bit \(c\) before starting the game. Therefore, the probability is presented in Equation (1):  
\[Adv_{\mathcal{A}}=[2 Pr[Succ_{GM0}]-1] \tag{1}\]  
\(Game_{1}\): An eavesdropping attack is performed by \(\mathcal{A}\) through the \(Execute\) query. \(\mathcal{A}\) attempts to compute a session key \(SK=h(UID_{i}||SI_{j})\oplus h(n_{i1}||n_{i2}||n_{i3})\) using messages transmitted over a public channel. Then, \(\mathcal{A}\) uses the \(Test\) query to determine whether the computed session key is real. In the proposed scheme, \(SI_{j},n_{i1},n_{i2}\), and \(n_{i3}\) are required to compute the session key. However, \(\mathcal{A}\) cannot calculate the session key; hence, the probability of success in this game is equal to that of \(Game_{0}\):  
\[Pr[Succ_{GM1}]=Pr[Succ_{GM0}] \tag{2}\]  
\(Game_{2}\): In this game, \(\mathcal{A}\) tries to forge a message using the \(Send\) and \(Hash\) queries. To do this, \(\mathcal{A}\) must determine a hash collision because messages are generated as hash values of secret parameters and random numbers. However, due to the one-way nature of the hash function, it is difficult for \(\mathcal{A}\) to determine the hash collision. Thus, based on the birthday paradox [49], Equation (3) can be derived:  
\[|Pr[Succ_{GM2}]-Pr[Succ_{GM1}]|\leq\frac{q_{h}^{2}}{2|Hash|} \tag{3}\]  
\(Game_{3}\): Similar to \(Game_{2}\), \(\mathcal{A}\) uses \(PUF\) and \(Send\) queries.