## 4 Security Analysis
### Security Properties  
ProVerif can analyze the properties of reachability, correspondence assertions, and observational equivalences. It is important to note that while ProVerif is sound, it is not complete. It means that if ProVerif determines that a property is satisfied, the model guarantees that it is valid. However, ProVerif may not be able to prove that a property holds. ProVerif uses queries that might be a fact or correspondence for security evaluations. Primarily, we query whether a term \(sec\) is secret for the attacker: query attacker \((sec)\). The query is a fact in the case of _reachability_, and we test whether the fact holds. A _correspondence_ is a form of \(X\to Y\), which means if \(X\) holds, then \(Y\) also holds. We define events in the model as important stages and test whether event \(a\) has been executed, and then whether event \(b\) was previously executed. The \(queryent:a(s,t)\to event:b(t,z)\). means that for all \(s,t\) and each occurrence of \(a(s,t)\), there is a previous occurrence of \(b(t,z)\) for some \(z\). To prove the one-to-one relationship, we apply injective correspondences. The \(queryinj-event:a(s,t)\to inj-event:b(t,z)\). means that for each occurrence of event \(a(s,t)\), there is a _distinct_ earlier occurrence of the event \(b(t,z)\) for some \(z\). We use the security queries and define six events demonstrated by Figure 7.  
Figure 6: Main process. In the registration phase, we apply injective correspondences for mutual authentication of the new drone, base station and registered drones. We prove new drone authentication with the nested correspondence: _query a1:bitstring,a2:bitstring;a3:bitstring,a4:bitstring; inj-event_(\(ND\)RegEnd(a4)) ==\(>\) (inj-event_(\(BSRegEnd(a3)\))==\(>\)(inj-event_(\(BSRegStart(a2)\))==\(>\)_inj-event_(\(ND\)RegStart(\(a1)\))))._  
With another nested correspondence, we show the authentication of the base station and the already registered drones: _query a1: bitstring,a2:bitstring,a3:bitstring,a4:bitstring; inj-event_(\(BSDRegEnD(a4)\)) ==\(>\) (inj-event_(\(BSRegInter(a3)\))==\(>\) (inj-event_(\(DRegStart(a2)\))==\(>\)_inj-event_(\(BSRegStart(a1)\))))._  
All the queries above return the value true. Therefore, from the security requirements, participant authentication, i.e., mutual authentication of the new drone, the already registered drones, and the base station, are held, and the secrecy of the symmetric keys is also maintained in our model. Moreover, all verifications are fulfilled in the registration. Therefore, parties confirm that the other party knows and can use the new symmetric key when the user verifies the base station response or the base station, and the drones check the MAC value with the random input value in the last step of the protocol (\(MAC_{K_{BND}}(rd),MAC_{K_{DND}}(rd)\)). The key freshness property is also achieved because every registration requires a Diffie-Hellman key exchange, which results in a new, random key. Since the listed security requirements hold, the protocol is secure against man-in-the-middle and replay attacks as well. ProVerif is based on the perfect cryptography assumption, which means cryptographic primitives, such as symmetric encryption or MAC, are ideal black boxes. The cryptographic primitives need to satisfy the required security properties. We extend the formal security analysis with an informal analysis in order to take into account the typical attacks against IoD systems. The following informal security analysis explicates that registration and communication phases are immune to several attacks, such as drone capture attacks, denial-of-service attacks or jamming attacks. * Drone capture attack: When physically capturing a drone, it is of the utmost importance to ensure that the attacker cannot extract any sensitive data. This precautionary measure is necessary to defend against potential breaches of secrecy of the information. In our case, the drone does not store the secret keys in the memory because of the PUF solution.