# A Secure Key Aggregate Searchable Encryption with Multi Delegation in Cloud Data Sharing Service
## 5 Security Analysis
### BAN Logic Analysis
#### 5.2.1 Logical Rules of BAN Logic  
The Logical rules of the BANlogic are:  
1. [label=**0.0**, ref=**0.0**]
2. _Jurisdiction rule :_ \[\frac{\omega\mid\equiv\sigma\mid\implies S,\ \ \omega\mid\equiv\sigma\mid\equiv ST}{ \omega\;\Big{|}\equiv S}\]
3. _Nonce verification rule :_ \[\frac{\omega\mid\equiv\#(ST),  
**Goal 1:**: \(CS|\equiv(R_{du})\),
**Goal 2:**: \(CS|\equiv DU_{j}|\equiv(R_{du})\),
**Goal 3:**: \(DU_{j}|\equiv(R_{cs})\),
**Goal 4:**: \(DU_{j}|\equiv CS|\equiv(R_{cs})\),  
5.2.3. Idealized Forms for Data Retrieve Phase  
The idealized forms are as following :  
\(M_{1}:\;DU_{j}\to CS:(HID_{j},T_{1},R_{du},DPK_{do})_{g^{j,As}}\)  
\(M_{2}:\;CS\to DU_{j}:(HID_{j},T_{1},R_{cs})_{g^{j,As}}\)  
5.2.4. Assumptions for Data Retrieve Phase  
The following assumptions are the initial state of the proposed scheme to achieve BAN logic proof.  
\(A_{1}:\;CS|\equiv(CS\xrightleftharpoons{\xi^{y,\cdot As}_{\xi^{y,\cdot As}}}DU_{j})\)  
\(A_{2}:\;DU_{j}|\equiv(DU_{j}\xrightleftharpoons{\xi^{y,\cdot As}_{\xi^{y,\cdot As }}}CS)\)  
\(A_{3}:\;CS|\equiv\#(R_{du})\)  
\(A_{4}:\;DU_{j}|\equiv\#(R_{cs})\)  
\(A_{5}:\;CS|\equiv DU_{j}\Rightarrow(R_{du})\)  
\(A_{6}:\;DU_{j}|\equiv CS\Rightarrow(R_{cs})\)  
5.2.5. Proof Using BAN Logic for Data Retrieve Phase  
Main proofs using rules and assumptions of the BAN logic are as the following steps :  
**Step 1:**: \(S_{1}\) can be obtained from \(M_{1}\)  
\(S_{1}:CS\lhd(HID_{j},T_{1},R_{du},DPK_{do})_{g^{j,As}}\).
**Step 2:**: For obtaining \(S_{2}\), we apply the message meaning rule with \(A_{1}\)  
\(S_{2}:CS|\equiv DU_{j}|\sim(HID_{j},T_{1},R_{du},DPK_{do})\).
**Step 3:**: For obtaining \(S_{3}\), we apply the freshness rule with \(A_{3}\)  
\(S_{3}:CS|\equiv\#(HID_{j},T_{1},R_{du},DPK_{do})\).
**Step 4:**: For obtaining \(S_{4}\), we apply the nonce verification rule with \(S_{2}\) and \(S_{3}\)  
\(S_{4}:CS|\equiv DU_{j}\equiv(HID_{j},T_{1},R_{du},DPK_{do})\).  
**Step 5:**: For obtaining \(S_{5}\), we apply the belief rule  
\[S_{5}:CS|\equiv DU_{j}|\equiv(R_{du}).\] **(Goal 2)**:
**Step 6:**: For obtaining \(S_{6}\), we apply the jurisdiction rule with \(A_{5}\)  
\[S_{6}:CS|\equiv R_{du}.\] **(Goal 1)**:
**Step 7:**: \(S_{7}\) can be obtained from \(M_{2}\)  
\[S_{7}:DU_{j}\lhd(HID_{j},T_{1},R_{cs})_{g}^{b_{j},A_{cs}}.\]
**Step 8:**: For obtaining \(S_{8}\), we apply the message meaning rule with \(A_{2}\)  
\[S_{8}:DU_{j}|\equiv CS|\sim(HID_{j},T_{1},R_{cs}).\]
**Step 9:**: For obtaining \(S_{9}\), we apply the freshness rule with \(A_{4}\)  
\[S_{9}:DU_{j}|\equiv\#(HID_{j},T_{1},R_{cs}).\]
**Step 10:**: For obtaining \(S_{4}\), we apply the nonce verification rule with \(S_{8}\) and \(S_{9}\)  
\[S_{10}:DU_{j}|\equiv CS|\equiv(HID_{j},T_{1},R_{cs}).\]
**Step 11:**: For obtaining \(S_{11}\), we apply the belief rule  
\[S_{11}:DU_{j}|\equiv CS|\equiv(R_{cs}).\] **(Goal 4)**:
**Step 6:**: For obtaining \(S_{12}\), we apply the jurisdiction rule with \(A_{6}\)  
\[S_{12}:DU_{j}|\equiv R_{cs}.\] **(Goal 3)**:  
Thus, our scheme has completed the proof that it provides mutual authentication for data retrieve phase. BAN logic proof of authentication for delegation phase is similar to the above proof. Therefore, our scheme can provide secure mutual authentication.