# A Blockchain-Based Secure Inter-Hospital EMR Sharing System
## 4 Security Analysis  
### Mutual Authentication  
The BAN logic proof model is applied in order to prove that mutual authentication is achieved between different parties in each phase of the proposed scheme. In the initial treatment authentication and communication phase of the proposed scheme, the main goal of the scheme is to authenticate the session key establishment between the patient, \(P\), and hospital A, \(HA\). \begin{tabular}{l l} \(G1\): & \(P|\equiv P\stackrel{{SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G2\): & \(P|\equiv HA|\equiv P\stackrel{{SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G3\): & \(HA|\equiv P\stackrel{{SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G4\): & \(HA|\equiv P|\equiv P\stackrel{{SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G5\): & \(P|\equiv ID_{HPA}\) \\ \(G6\): & \(P|\equiv HA|\equiv ID_{HPA}\) \\ \(G7\): & \(HA|\equiv ID_{PAT}\) \\ \(G8\): & \(HA|\equiv P|\equiv ID_{PAT}\) \\ \end{tabular}   
According to the initial treatment authentication and communication phase, BAN logic is applied in order to produce an idealized form as follows: \begin{tabular}{l l} \(M1\): & \((<ID_{PAT},R_{PAT},T_{PAT}>_{PK_{HPA}},<H(SEK_{AP},T_{HPA})>_{CHK_{AP}})\) \\ \(M2\): & \((<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{PAT}},<H(SEK_{AP},T_{PAT})>_{CHK_{PA}})\) \\ \end{tabular}   
To analyze the proposed scheme, the following assumptions are made: \begin{tabular}{l l} \(A1\): & \(P|\equiv\#(T_{PAT})\) \\ \(A2\): & \(HA|\equiv\#(T_{PAT})\) \\ \(A3\): & \(P|\equiv\#(T_{HPA})\) \\ \(A4\): & \(HA|\equiv\#(T_{HPA})\) \\ \(A5\): & \(P|\equiv HA|\Rightarrow P\stackrel{{SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \end{tabular}   
_A6_: \(HA|\equiv P|\Rightarrow P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\)  
_A7_: \(P|\equiv HA|\Rightarrow ID_{HPA}\)  
_A8_: \(HA|\equiv P|\Rightarrow ID_{PAT}\)  
According to these assumptions and the rules of BAN logic, the main proof of the initial treatment authentication and communication phase is as follows:  
* Hospital A, \(HA\), authenticates the patient, \(P\). We derive the following statement by \(M1\) and the seeing rule: \(HA\triangleleft(<ID_{PAT},R_{PAT},T_{PAT}>_{PK_{HPA}}<H(SEK_{AP},T_{HPA})>_{ CHK_{AP}})\) (Statement 1) We derive the following statement by \(A2\) and the freshness rule: \(HA\big{|}\equiv\#(<ID_{PAT},R_{PAT},T_{PAT}>_{PK_{HPA}}<H(SEK_{AP},T_{HPA})>_{ CHK_{AP}})\) (Statement 2) We derive the following statement by (Statement 1), \(A4\), and the message meaning rule: \(HA\big{|}\equiv P|\sim(<ID_{PAT},R_{PAT},T_{PAT}>_{PK_{HPA}}<H(SEK_{AP},T_{HPA})>_{ CHK_{AP}})\) (Statement 3) We derive the following statement by (Statement 2), (Statement 3), and the nonce verification rule: \(HA\big{|}\equiv P\big{|}\equiv(<ID_{PAT},R_{PAT},T_{PAT}>_{PK_{HPA}}<H(SEK_{AP},T_{ HPA})>_{CHK_{AP}})\) (Statement 4) We derive the following statement by (Statement 4) and the belief rule: \(HA\big{|}\equiv P\big{|}\equiv P\stackrel{{ SEK_{AP}}}{{ \leftrightarrow}}HA\) (Statement 5) We derive the following statement by (Statement 5), \(A6\), and the jurisdiction rule: \(HA\big{|}\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) (Statement 6) We derive the following statement by (Statement 6) and the belief rule: \(HA\big{|}\equiv P|\equiv ID_{PAT}\) (Statement 7) We derive the following statement by (Statement 7), \(A8\), and the jurisdiction rule: \(HA\big{|}\equiv ID_{PAT}\) (Statement 8)
* The patient \(P\) authenticates the hospital A \(HA\).