# FAIDM for Medical Privacy Protection in 5G Telemedicine Systems
## 4 Security Analysis
### Formal Verification Using BAN Logic  
BAN logic has become a widely accepted and well-known logical methodology for analyzing security of schemes [54; 55; 56; 57]. The goal of BAN logic is to verify the exchanged information and the belief relationship among communicating parties and analyze protocols by deriving beliefs to proof that honest and legitimate parties can correctly execute and complete a protocol [54; 66; 67; 68]. We apply BAN logic [54] to prove the authenticity of our scheme. The notations used in BAN logic [54] analysis are defined as follows. \(P\) and \(Q\) are principles, \(X\) and \(Y\) are statements, \(C\) is channel, \(r\) and \(w\) are set of readers and writers respectively, and \(K\) is encryption key. \(P\sqsubseteq X\) denotes that \(P\) believes \(X\); \(P\sqcap X\) denotes that \(P\) once said \(X\); \(C(X)\) means that \(X\) is transited via channel \(C\); \(r(C)\) and \(w(C)\) denotes as the set of readers and writers of \(C\) respectively. \(P\)\(\lessdot\)\(C(X)\) means that \(P\) sees \(C(X)\). \(X\) is transited via \(C\) and can be observed by \(P\), and \(P\) must be a reader of \(C\) to read \(X\). \(P\)\(\lessdot\)\(X\)\(\mid\)\(C\) means that \(P\) sees \(X\) via \(C\). \((X)_{K}\) denotes that \(X\) is encrypted with the key \(K\). \(P\)\(\lessdot\)\(Q\) means that \(P\) and \(Q\) can establish a secure communication channel by using \(K\). The logical postulates in BAN logic [54] are described using rules below.  
Rule 1. \(\frac{P\lessdot\)\(C(X)\), \(Per(C)}{P\sqsubseteq(P\)\(X)\), \(P\)\(\lessdot\)\(X\)}: If \(P\) receives and reads \(X\) via \(C\), then \(P\) believes that \(X\) has arrived on \(C\) and \(P\) sees \(X\).  
Rule 2. \(\frac{P\lessdot\)\(C(X)\), \(P\)\(\lessdot\)\(X\)}: If \(P\) sees a hybrid message \((X\), \(Y)\), then \(P\) sees \(X\) and \(Y\) separately.  
Rule 3. \(\frac{P\sqsubseteq(P\)\(\lessdot\)\(X\)\(\Rightarrow\)\(\{P,Q\})}{P\sqsubseteq(P\)\(\lessdot\)\(X\)\(\Rightarrow\)\(Q\)\(\mid\)\(\sim\)\(\sim\)\(\sim\)}\): If \(P\) believes that \(C\) can only be written by \(P\) and \(Q\), then \(P\) believes that if \(P\) receives \(X\) via \(C\), then \(Q\) said \(X\).  
Rule 4. \(\frac{P\sqsubseteq(Q\)\(\sim\)\(X\)\(\Rightarrow\)\(P\)\(\sqsubseteq(Q\)\)\(\sim\)\(\sim\)}\): If \(P\) believes that \(Q\) said a hybrid message \((X\), \(Y)\), then \(P\) believes that \(Q\) has said \(X\) and \(Y\) separately.  
Rule 5. \(\frac{P\sqsubseteq(\)\(\(\Based on to the assumptions and logical analyses, the proposed scheme must realize goals in Table 3.  
To accomplish the Goal 1, we have Equations (42) and (43). Equations (42) and (43) must hold because of Rule 5 and A5.  
\[CN_{ij}\ |\equiv(\overset{\omega_{t}}{\rightarrow}_{ECMDH(\mathit{specific})} CN_{ij}) \tag{42}\]  
\[CN_{ij}\ |\equiv(\overset{\omega_{t}}{\rightarrow}_{ECMDH(\mathit{public})} GW_{t}) \tag{43}\]  
Next, we have Equations (44) and (45) that must hold because of A3 and Rule 8 to accomplish Equation (43).  
\[CN_{ij}\ |\equiv(\overset{\omega_{t}}{\rightarrow}_{ECMDH(\mathit{public})} GW_{t},\ C_{CN_{ij},\ GW_{t}}(P_{ij},\ P_{t},\omega_{t})_{\delta_{CW_{ij}+CN_{ij}}} \omega_{t})\ \rightarrow(\overset{\omega_{t}}{\rightarrow}_{ECMDH(\mathit{public})} GW_{t}) \tag{44}\]  
\[CN_{ij}\ |\equiv(GW_{t}\ |\ \sim\overset{\omega_{t}}{\rightarrow}_{ECMDH( \mathit{public})}GW_{t}) \tag{45}\]  
We have Equation (46) which must hold because of Rule 6 and 7 and A4 to accomplish Equation (45).  
\[CN_{ij}\ |\equiv\#(\overset{\omega_{t}}{\rightarrow}_{ECMDH(\mathit{public})} GW_{t}) \tag{46}\]  
We have Equations (47)-(49) which must hold because of Rule 1, 2, and 3, and A1 and A2 to accomplish Equation (46).  
\[CN_{ij}\ \in\ r(C_{GW_{t},\ CN_{ij}}) \tag{47}\]  
\[CN_{ij}\ |\ \equiv\