# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions  
Using ProVerif, we can verify if the adversary can access the security parameters by reaching the state where those parameters are available. In our protocol, the private key of HN (skHN), a Long-term key at UE/HN (uk), and the Long-term identity (SUPI) were queried to verify their secrecy. The sequence of the protocol can also be verified by modeling how the messages are processed and exchanged among UE, SN and HN. Those can be verified using assertions consisting of events that represent message processing and delivery. We utilize the same naming rules for events with [29]. Therefore, for a query \(x\), we formally define events as follows:  
* _event UESendReqSN(:)_: UE sends a connection request with the required parameters to SN in Step 1.1. * _event SNRecReqUE(:)_: SN receives a connection request with the required parameters from UE in Step 1.2. * _event SNSendReqHN(:)_: SN sends a connection request with the required parameters to HN in Step 1.2. * _event HNRecReqSN(:)_: HN receives the result of a connection request with the other relevant parameters from SN in Step 1.3. * _event HNSendResSN(:)_: HN sends the result of a connection request with the other relevant parameters to SN in Step 2.1. * _event SNRecReHN(:)_: SN receives the result of a connection request with the other relevant parameters from HN in Step 2.2. * _event SNSendResUE(:)_: SN sends the result of a connection request with the other relevant parameters to HN in Step 2.2. * _event UERecResSN(:)_: UE receives the result of a connection request with the other relevant parameters from SN in Step 2.3. * _event UESendConSN(:)_: UE sends authentication parameters to SN in _Case iii_ in Step 2.3. * _event SNSendConHN(:)_: SN forwards (\(RES^{*}\)) to HN in _Case iii_ in Step 2.3. * _event SNRecConUE(:)_: SN receives (\(RES^{*}\)) from UE _Case iii_ in Step 2.3. * _event HNRecConSN(:)_: HN receives (\(RES^{*}\)) from SN _Case iii_ in Step 2.3. * _event HNSendSUPIS(:)_: HN sends (\(SUPI,K_{SEAF}\)) to SN in _Case iii_ in Step 2.3. * _event SNRecSUPHIN(:)_: SN receives (\(SUPI,K_{SEAF}\)) from HN in _Case iii_ in Step 2.3. Using the events described above, we can formally verify the hypothesis \"event A ==> event B\", which means that, without the execution of event B, event A cannot be executed. For example, the first two lines of the following ProVerif code of Process Verification imply that SN sends a connection request with the required parameters to HN only if HN receives the result of a connection request with the other relevant parameters from SN. The following are the all events we verified in the implementation. **Process Verification**  
``` query a:bitstring,b:bitstring; event(HNRecReqSN(a)) ==> event(SNSendReqHN(b)). query a:bitstring,b:bitstring; event(SNRecResHN(a)) ==> event(HNSendResSN(b)). query a:bitstring,b:bitstring; event(UERecResSN(a)) ==> event(SNSendResUE(b)). query a:bitstring,b:bitstring; event(SNRecConUE(a)) ==> event(UESendConSN(b)). query a:bitstring,b:bitstring; event(HNRecConSN(a)) ==> event(SNSendConHN(b)). query a:bitstring,b:bitstring; event(SNRecSUPHIN(a)) ==> event(HNSendSUPIS(b)). #### 5.2.4 Verification Results

We execute our ProVerif code on the ProVerif online demo website. As a result of the verification, we can conclude that the attacker cannot access the security keys in any state of the process. Moreover, all the sequences of executions of UE, SN, and HN are verified as defined in the protocol. The summary of the verification results is as follows: