# SENTINEL: A Secure and Efficient Authentication Framework for Unmanned Aerial Vehicles
## 8 Security Analysis  
### Formal Security Analysis Using ProVerif  
To analyze the security of SENTINEL, we present a brief formal security evaluation of the SENTINEL using ProVerif [30], which is an automatic symbolic protocol verifier, and popularly used for verifying cryptographic protocols (e.g., [31; 32]). First of all, we define a set of cryptographic primitives \(F\) that is used to verify the key agreement procedure. \(F\) is used for the drone as well as the ground station (see the ProVerif code in Listing 1). There are two types of encryption methods: ENC for symmetric key encryption and AENC for public key encryption. PBKDF is used to create the flight session key, and salt consists of the nonce of the drone and the ground station. List of functions required for the key agreement procedure for both drone and ground station. Functions:  
F={SIGN, CheckSIGN, SIGN_KEY, SIGN_CERT, GetCERT, CheckSIGN_CERT, ENC, DEC, AENC, ADEC, PBKDF}  
SIGN(private key, data) = signed value. CheckSIGN(signed value, public key) = True or False. SIGN_KEY(key, private key) = singed value. SIGN_CERT(certificate, private key) = singed value. GetCERT(signed value) = certificate. CheckSIGN_CERT(signed value, public key) = True or False. ENC(key, data) = ciphertext. DEC(key, ciphertext) = data. AENC(public key, data) = ciphertext. ADEC(private key, ciphertext) = data. PBKDF(secret value, salt, iteration) = hashed value. Listings 2 and 3 show the procedures performed for key agreement between drone \(d\) and ground station \(gs\). In our ProVerif model, \(d\) initially holds its private key \(sk_{d}\), public key \(pk_{d}\), certificate \(cert_{d}\) and \(CA\)'s public key \(pk_{CA}\). \(gs\) also holds its private key \(sk_{gs}\), public key \(pk_{gs}\), certificate \(cert_{gs}\) and \(CA\)'s public key \(pk_{CA}\). Both \(cert_{d}\) and \(cert_{gs}\) can be verified using \(pk_{CA}\). As mentioned in Section 3.2, we set an active attacker who has complete control of the communication channel between \(d\) and \(gs\). The attacker can read, modify, delete and inject messages. The attacker is also able to manipulate the data. In the step 2a of Figure 3, \(gs\) sends its random nonce \(n_{gs}\) along with the drone's random nonce \(n_{d}\) after being signed with the private key of ground station \(sk_{gs}\). We defined the sign function (denoted as SIGN(private key, data) = signed value) and used it as Sig(\(sk_{gs}\), signed nonce) in Listing 3. To check the validity of the signed value, \(d\) uses both GetCERT and GetPKEY. In the step 3 of Figure 3, \(d\) first obtains \(gs\)'s public key \(pk_{gs}\) using GetCERT(received \(cert_{gs}\)) in Listing 2. Then, \(d\) uses CheckSIGN(singed nonce, \(pk_{gs}\)) to check the validity of the singed nonce. To create a flight session key \(k_{d}\), both \(d\) and \(gs\) use PBKDF(\(pms\), concatenated nonce (\(n_{d}\|n_{gs}\)). ```
Stored information: (\(sk_{d}\), \(pk_{d}\), \(cert_{d}\), \(pk_{CA}\)) Process: Drone\(\triangleq\) new \(id\). new \(n_{d}\). out(ch, (\(id\), \(n_{d}\), \(cert_{d}\))). in(ch, (\(signed\) nonce, received \(cert_{gs}\))). let \(cert_{gs}\) = GetCERT(received \(cert_{gs}\)) in let valid \(cert_{gs}\) = CheckSIGN_CERT(received \(cert_{gs}\), \(pk_{CA}\)) in if \(cert_{gs}\) = valid \(cert_{gs}\) then let \(pk_{gs}\) = GetPKEY(\(cert_{gs}\)) in let received nonce = GetNESS(signed nonce) in let valid received nonce = CheckSIGN(signed nonce, \(pk_{gs}\)) in if received nonce = valid received nonce then in(ch, signed \(pms\)). let encrypted \(pms\) = GetNESS(signed \(pms\)) in let valid encrypted \(pms\) = CheckSIGN(signed \(pms\), \(pk_{gs}\)) in if encrypted \(pms\) = valid encrypted \(pms\) then let \(pms_{d}\) = ADEC(encrypted \(pms\), \(sk_{d}\)) in let \(k_{d}\) = PBRDF(\(pms_{d}\), received nonce) in event acceptsDrone(\(k_{d}\)). out(ch, ENC(s, \(k_{d}\))). ```  
Listing 2: Procedure performed on drone \(d\) for key agreement.