## 4 Security Analysis of the Proposed Protocol
### Formal Security Proof
#### 4.1.1 Basis for Security Proof  
In this study, three primary participants within our protocol \(\mathbf{P}\) are identified as follows: a physician denoted as \(U_{i}\), a gateway node referred to as \(GWN\), and a body area sensor node labeled as \(MS_{j}\). Before initiating the simulation, the simulator selects the RSA cryptosystem, employing two large prime numbers \(p\) and \(q\) with equal bit lengths, i.e., \(|p|=|q|=n\). Subsequently, \(U_{i}\) selects a set of personal information \(\{ID_{i},PW_{i}\}\). Simultaneously, \(GWN\) generates a long-term key pair \(\{x,y\}\), and \(MS_{j}\) owns an identity-secret key pair \(\{MIS_{j},x_{j}\}\). During the proof process, three entities will instantiate \(U_{i},GWN\), and \(MIS_{j}\), with their respective instances denoted as \(\Pi^{u}_{u_{i}},\Pi^{g}_{GWN}\), and \(\Pi^{uu}_{MS_{j}}\). For the sake of simplicity, these instances can collectively be marked as \(\Pi^{t}\) when distinguishing them is unnecessary. Moreover, each instance is treated as an oracle. This implies that if a message input is valid, invalid, or null, the oracle's state accordingly is an acceptance, rejection, or \"\(\bot\)\", respectively, where \"\(\bot\)\" indicates that there is no response to the input. Subsequently, we introduce certain terms that are pertinent to this proof:  
Accepted State: An instance \(\Pi^{t}\) reaches an accepted state upon receiving the final expected protocol message. Notably, the ordered concatenation of all exchanged messages (both sent and then received) shapes the session identifier for the current session of \(\Pi^{t}\). Partnering: Instances \(\Pi^{t_{1}}\) and \(\Pi^{t_{2}}\) are considered partnered if they simultaneously meet the following criteria: (a) both are in an accepted state, (b) mutual authentication has occurred, and they share an identical session identifier. Adversary: In this context, adversary \(\mathcal{A}\) can interact solely with honest entities by initiating query oracles and controlling the simulator. \(\mathcal{A}\) aims to compromise the security of authentication messages and re-construct the session key within protocol \(\mathbf{P}\). The queries that \(\mathcal{A}\) can launch include the following:  
* Execute \((\Pi^{u}_{u_{i}},\Pi^{g}_{GWN},\Pi^{m}_{MS_{j}})\): This query allows \(\mathcal{A}\) to simulate the entire authentication process and access exchanged messages between \(U_{i},GWN\), and \(MS_{j}\). * Send \((\Pi^{t},m)\): \(\mathcal{A}\) can send message \(m\) and conduct an active attack on instance \(\Pi^{t}\). If \(l\) is valid and \(\Pi^{t}\) has received \(m\), the simulator responds to \(\mathcal{A}\) with the computation of \(m\); otherwise, this query is terminated. * Reveal \((\Pi^{t})\): This query results in revealing the session key calculated by \(\Pi^{t}\) and its partner to adversary \(\mathcal{A}\). * Corrupt \((\Pi^{u}_{u_{i}},\alpha)\): In this query, \(\mathcal{A}\) can obtain authentication factors associated with \(U_{i}\) based on value \(\alpha\). Specifically, the oracle exposes the password to \(\mathcal{A}\) when \(\alpha=0\) and exposes the data stored in the registration package to \(\mathcal{A}\) when \(\alpha=1\). * Corrupt \((\Pi^{g}_{GWN})\): In this query, \(\mathcal{A}\) can gain access to the long-term key \(x\) possessed by \(GWN\). * Corrupt \((\Pi^{m}_{MS_{j}})\): This query enables \(\mathcal{A}\) to obtain the secret value of \(MS_{j}\). Freshness: An instance of \(\Pi_{u_{i}}^{u}\), \(\Pi_{GWN}^{\mathcal{S}}\), or \(\Pi_{MS_{j}}^{m}\) is deemed fresh if the session key between \(U_{i}\) and \(MS_{j}\) remains undisclosed to \(\mathcal{A}\) via the aforementioned reveal query. Test (\(\Pi^{\prime}\)): This query assesses the semantic security of session key \(SK\). In this query, \(\mathcal{A}\) can make only one inquiry. Considering protocol \(\mathbf{P}\), instance \(\Pi^{\prime}\) can only either be \(\Pi_{u_{i}}^{u}\) or \(\Pi_{MS_{j}}^{m}\). Formally, if test \(\left(\Pi^{\prime}\right)\) has been queried before, the query outputs \"\(\bot\)\" (null).