## 5 Security Analysis
### Informal Security Analysis
The verification steps (\(H(RP^{\prime}_{ID_{O}}\|Salt_{1})==RPMD_{ID_{O}}\) and \(T^{\prime}_{ID}==T_{ID}\)) serve as strong integrity checks. Any modification leads to immediate verification failure, ensuring that altered messages are reliably detected. This robustly meets requirement 8. * and untraceability: The operator's identity \(ID_{O}\) is explicitly sent in message \(M_{1}\). While this design choice enables the GCS to identify the operator, it inherently means that an adversary can potentially link communication sessions to a specific operator ID. Therefore, full user anonymity and untraceability (requirement 9) are only partially met in the current design. Future work could effectively explore the integration of pseudonyms, as discussed in [2; 6; 29] to significantly enhance this feature. * forward secrecy (PFS): The session key KS depends on the operator's long-term local password \(P_{ID_{O}}\). If \(P_{ID_{O}}\) were to be compromised (e.g., if an attacker somehow extracted it from a stolen OD and brute-forced it offline), past session keys (KS) derived using that \(P_{ID_{O}}\) could potentially be compromised. Therefore, perfect forward secrecy (requirement 10) is limited in the current design. * to stolen verifier attack: The GCS stores \(RPMD_{ID_{O}}\), which is a salted hash digest of \(RP_{ID_{O}}\). Crucially, the actual \(RP_{ID_{O}}\) is stored encrypted (\(C_{BP}\)) on the OD and is derived via biometric authentication and a local PIN. Stealing \(RPMD_{ID_{O}}\) from the GCS database does not directly reveal \(RP_{ID_{O}}\) or \(P_{ID_{O}}\), due to the one-way property of hash functions and the effective use of salting. This makes the protocol robustly resistant to stolen verifier attacks, which [PERSON]'s cryptanalysis [19] highlights as a significant vulnerability in other schemes. This effectively addresses a critical aspect of requirement 11. * (lightweight design): The protocol relies exclusively on lightweight symmetric cryptographic operations (AES encryption/decryption) and efficient hash functions (SHA-256), along with key derivation functions (KDFs). These operations are computationally efficient and are thus exceptionally well suited for resource-constrained IoD components like operator devices and drones [1; 11]. This design choice strongly meets requirement 12. ### BAN Logic Analysis  
(Follows standard BAN logic proof structure [14; 24; 28]). The goal is to show that \(OD\mid\equiv OD\stackrel{{ KS}}{{\rightarrow}} GCS\) and \(GCS\mid\equiv GCS\stackrel{{ KS}}{{\rightarrow}} OD\). Initial Assumptions (Axioms)  
1. \(TA\mid\equiv(ID_{O},P_{ID_{O}},RP_{ID_{O}},Salt_{1})\). 2. \(OD\mid\equiv TA\Rightarrow(RP_{ID_{O}},HD_{O})\). 3. \(GCS\mid\equiv TA\Rightarrow(ID_{O},\text{key material for }P_{ID_{O}},RPMD_{ID_{O}},Salt_{1})\). 4. \(U_{O}\stackrel{{ K_{O}}}{{\leftrightarrow}} OD\). 5. \(OD\mid\equiv\text{fresh}(T_{ID}),OD\mid\equiv\text{fresh}(PIN)\). * \(OD\mid\equiv P_{ID_{O}}\). * \(GCS\mid\equiv P_{ID_{O}}\). * \(OD,GCS\mid\equiv(KDF(S,T)\implies K_{S,T})\). * Idealized Protocol Messages
* \(OD\to GCS:ID_{O},T_{ID},\{PIN,T_{ID},RP_{ID_{O}}\}_{KS}\)
* \(GCS\to OD:\{PIN\}_{KS^{\prime}}\) Analysis Sketch
* 1. OD sends M1. OD believes it shares \(P_{ID_{O}}\) with GCS (via TA's provisioning of \(RP_{ID_{O}}\) and shared knowledge of \(P_{ID_{O}}\)'s function) to compute KS. OD believes the contents of \(\{PIN,T_{ID},RP_{ID_{O}}\}_{KS}\) were intended for GCS and are fresh due to \(T_{ID}\) and PIN. * 2. GCS receives M1. GCS computes \(KS_{GCS}\) using \(P_{ID_{O}}\) (from its knowledge of \(ID_{O}\)'s associated random password and the \(T_{ID}\) from \(M_{1}\)). Using the Message-Meaning Rule on \(\{X\}_{KS_{GCS}}\) (where \(X=(PIN,T_{ID},RP_{ID_{O}})\)), GCS deduces \(GCS\mid\equiv OD\mid\sim X\). * 3. GCS verifies the freshness of \(T_{ID}\) by checking \(T_{ID}>LT_{O}\) and \(T_{current,GCS}-T_{ID}\leq\Delta_{t}\). Since \(T_{ID}\) is fresh, it believes \(\#(X)\). By the Nonce Verification Rule, \(GCS\mid\equiv OD\mid\equiv X\).