# DOSS Protocol for Data Caching and Sharing Security in a 5G Network
## 6 Verifying of DCSS Protocol
### Formal Verification Using ProVerif  
In ProVerif, the protocol modelling is composed of declaration, process macros, and main processes. With queries used in the rectification of the correctness and secrecy of a protocol. Using declarations of types, functions, queries, and events, the ProVerif code is used to effectively specify the protocol. Free names are free variables that are known to the public, globally known whereas bound names are locally known by the process such as the public channel for communication, [private] excludes names from the attacker [54].  
Specification includes the following:  
* Functions: fun sign(bitstring, skey): bitstring,
* Key: type key.
* Private and public names: free fid:id [private]. free kues:key [private] free pubChannel: channel.
* Queries: Queries on secrecy, reachability, and authentication. A query of the attacker's knowledge attacker(M) is used to specify a secrecy property. The attacker  
\begin{table}
\begin{tabular}{c c} \hline \hline
**Term** & **Grammar** \\ \hline a, b, c, k, s & name \\ x, y, z & variable \\ M,N := & terms \\ h(D1,...,Dn) & function application \\ f(M1,...,Mn) & constructor application \\ D := & expressions \\ fail & failure \\ P,Q := & processes \\ out(N,M); P & output \\ in(N, x : T); P & input \\!P & iP replication \\
0 & nil \\ P | Q & parallel composition \\ new a : T; P & restriction \\ let x : T = D in P else Q & expression evaluation \\ if M then P else Q & conditional \\ \hline \hline \end{tabular}
\end{table}
Table 3: Core Language: Term and Process Grammar.  
may have knowledge of M if the fact attacker(M) can be derived from the horn clauses. There is no way for the attacker to learn about M if the fact attacker(M) cannot be derived from the clauses. With reachability, the query query attacker(K) is also used to debug the model of the protocol to check a particular branch is reachable or not. query k: bitstring; event(endServer(k)). The correspondence assertions are used to specify authentication properties as event(e1(M)) event(e2(M)). If all clauses that conclude event e1 include event e2 in their hypotheses, then event e1 can only be derived when event e2 is true, proving the correspondence assertion [54]. In the case of the DCSS protocol, the following is queried: query attacker (eid). query attacker (kue3a) are used to test the secrecy of the message, \(FID\) and key \(K_{UESS}\), respectively, while query U:host, SS:host, K:key; event (endSS (U,SS,K)) ==> event(beginUE (U,SS,K)) is used to test events relationships (authentication).
* Events: Querying events using correspondence assertion to test the relationship between events. (i) Event correspondence uses syntax to query a basic correspondence assertion, query x1 :t1,..., xn :tn ; event (e(M1,...,Mj)) ==> event(e'(N1,...,Nk) ). Where terms M1,....,Mj,N1,...,Nk are built by the constructors applied to the variables x1,...., xn of types t1,..., tn and e, e' are events. (ii) While the injective correspondence assertions are used to capture one-to-one relationship and denoted as query xi:t1,.., xn:tn ; inj-event(e(M1,..,Mj)) ==> inj-event (e'(N1,..,Nk) ). The correspondence asserts that there is a distinct earlier occurrence of the event e'(N1,...,Nk) for each occurrence of the event e(M1,...,Mj). [54].
* Process: The protocol encoded using the main process and the process macros for the participating entities to allow sub-process being defined; ((!procUE(hostU)) for the UE (!procAAA(hostA)) for the SPAAA and (!procSS (hostSS)) for SS. The main process also starts off with several copies of the system entities \(UE\), \(SPAAA\), \(SS\) using the required parameters denoting several roles sessions as explained in the message exchange.