# DOSS Protocol for Data Caching and Sharing Security in a 5G Network
## 6 Verifying of DCSS Protocol
### DCSS Protocol Formal Analysis
#### 6.3.2 Attack Derivation and Trace  
**TRACE 1**  
1 The attacker has some term A'_15173. attacker(A'_15173).  
2 The attacker has some term kue3a_15172. attacker(Kue3a_15172).  
3 The attacker initially knows hostU[]. attacker(hostU[])  
4 Using the function 3-tuple the attacker may obtain (hostU[], hostU[], kue3a_15172). attacker((hostU[],hostU[], kue3a_15172)).  
5 new skue: skey creating skue_15181 at {1}  
6 new sksks: sksey creating sks_15182 at {2}  
7 new skaaa: sksey creating ska_15183 at {3}  
8 out(c, \"M\") with \"M = pk(skue_15181) at {6}  
9 out(c, \"M_15346) with \"M_15346 = spk(skss_15182) at {8}  
10 out(c, \"M_15427) with \"M_15427 = spk(skaaa_15183) at {10}  
11 in(c, a_15179) at {12} in copy a_15180  
12 in(c, (hostU,hostU,a)) at {24} in copy a_15178  
13 get keys(hostU,hostU,a) at {57} in copy a_15180  
14 new skue_37: skey creating skue_15552 at {13} in copy a_15180  
15 new fid_39: id creating fid_15554 at {15} in copy a_15180  
16 new vacp: bitstring creating vacp_15560 at {21} in copy a_15180  
17 get keys(hostU,hostSS,kuess) at {56} in copy a_15180  
18 event endUE(hostU,hostSS,kuess) at {25} in copy a_15180 (goal)  
19 The event endUE(hostU,hostSS,kuess) is executed.  
20 A trace has been found.  
21 RESULT event(endUE(U_110,SS_111,K_112)) ==>  
event(beginSS(U_110,SS_111,K_112)) is false.  
**TRACE 2**  
22 event endUE(hostU,hostSS,kuess) at {25} in copy a_19431 (goal)  
23 The event endUE(hostU,hostSS,kuess) is executed in session a_19431.  
24 A trace has been found.  
25 RESULT inj-event(endUE(U_116,SS_117,K_118)) ==>  
inj-event(beginSS(U_116,SS_117,K_118)) is false.  
The attacker's actions are explained in derivations and trace steps concisely as shown in Figure 5, with some text omitted for simplicity. The two attack traces follow similar steps but have varying inputs, outputs, and events as follows.  
* In trace 1, Line 1-4 are steps taken by the attacker, indicating that attacker may know UE, therefore may also know key kue3a using the 3-tuple function in line 4. The attacker may have received message _A'_15173 by eavesdropping on the public channel at input [12] uses this knowledge to obtain _kue3a_15172_. Line 5-7 at input [1, 2, 3, 4] corresponds to creation and insertion of keys on public channel. Line 9-11 at output [6, 7, 8, 9, 10] correspondence with the attacker saving the keys in new variables \"M\" = pk(skue_15181), \"M_15346 = spk(sksss_15182) and \"M_15427 = spk (skaaa_15183) for reuse later. Line 11 at [12] the attacker has session copy a_15180 with _UE_ pretending to be _SPAAA_ as _I_SPAAA_ sending a_15179 to _UE_ after eavesdropping on the channel. On line 12 the attacker obtains message hostU,hostU,a that includes the key for session between _UE_ and _SS_ in session copy a_15178. The attacker eavesdrops on insertion of keys _KUESS_ at input [56] and _KUE3A_ input [57], respectively, in session copy a_15180. On line 14 _UE_ creates primitives at [13, 14, 15, 16, 17, 18, 19, 20, 21], sends them to _SPAAA_ start the protocol run. On line 18 the attacker was able to achieve is his goal in session copy a_15180 (goal) with _UE_, when the event endUE(hostU,hostSS,kuess) is executed. With _UE_ ending the protocol thinking it was talking to \(SS\) while \(UE\) never run the protocol with \(SS\). The attack is on non-injective agreement on line 21.
* In trace 2, the same steps, inputs, and outputs but in different sessions. In this trace the attacker achieves his goal in session copy a_19431 (goal) with \(UE\), when the event endUE(hostU, hostSS, kuess) is executed. The attack is against injective agreement a one-to-one relationship correspondence in session copy a_19431 on line 25.