# A Blockchain-Based Secure Inter-Hospital EMR Sharing System
## 4 Security Analysis
### Mutual Authentication
  
To analyze the proposed scheme, the following assumptions are made: \begin{tabular}{l l} \(A9\): & \(P|\equiv\pi(T_{PAT2})\) \\ \(A10\): & \(HB|\equiv\pi(T_{PAT2})\) \\ \(A11\): & \(P|\equiv\pi(T_{HPB})\) \\ \(A12\): & \(HB|\equiv\pi(T_{HPB})\) \\ \(A13\): & \(P|\equiv HB|\Rightarrow P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(A14\): & \(HB|\equiv P|\Rightarrow P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(A15\): & \(P|\equiv HB|\Rightarrow ID_{HPB}\) \\ \(A16\): & \(HB|\equiv P|\Rightarrow ID_{PAT}\) \\ \(A17\): & \(HB|\equiv\pi(T_{HPB2})\) \\ \(A18\): & \(HA|\equiv\pi(T_{HPB2})\) \\ \(A19\): & \(HB|\equiv\pi(T_{HPA2})\) \\ \(A20\): & \(HA|\equiv\pi(T_{HPA2})\) \\ \end{tabular}   
\(A21\): \(H\!B|\equiv HA|\Rightarrow HB\stackrel{{\text{SEK}_{AB}}}{{ \leftrightarrow}}HA\)  
\(A22\): \(HA|\equiv HB|\Rightarrow HB\stackrel{{\text{SEK}_{AB}}}{{ \leftrightarrow}}HA\)  
\(A23\): \(H\!B|\equiv HA|\Rightarrow ID_{HPA}\)  
\(A24\): \(HA|\equiv HB|\Rightarrow ID_{HPB}\)  
According to these assumptions and the rules of BAN logic, the inter-hospital authentication and communication phase is as follows:  
\(c.\) Hospital B, \(HB\), authenticates the patient, \(P\). We derive the following statement by \(M3\) and the seeing rule:  
\(HB\triangleleft(<ID_{PAT},R_{PAT},T_{PAT2}>_{PK_{HWB}}<H(SEK_{BP},T_{HPB})>_{ CHK_{BP}}\right)\) (Statement 17)  
We derive the following statement by \(A10\) and the freshness rule:  
\(HB|\equiv\#(<ID_{PAT},R_{PAT},T_{PAT2}>_{PK_{HWB}}<H(SEK_{BP},T_{HPB})>_{ CHK_{BP}})\) (Statement 18)  
We derive the following statement by (Statement 17), \(A12\), and the message meaning rule:  
\(HB|\equiv P|\sim(<ID_{PAT},R_{PAT},T_{PAT2}>_{PK_{HPB}}<H(SEK_{BP},T_{HPB})>_{ CHK_{BP}})\) (Statement 19)  
We derive the following statement by (Statement 18), (Statement 19), and the nonce verification rule:  
\(HB|\equiv P|\equiv(<ID_{PAT},R_{PAT},T_{PAT2}>_{PK_{HPB}}<H(SEK_{BP},T_{HPB})>_{ CHK_{BP}})\) (Statement 20)  
We derive the following statement by (Statement 20) and the belief rule:  
\(HB|\equiv P|\equiv P\stackrel{{\text{SEK}_{BP}}}{{ \leftrightarrow}}HB\)  
We derive the following statement by (Statement 21), \(A14\), and the jurisdiction rule:  
\(HB|\equiv P\stackrel{{\text{SEK}_{BP}}}{{ \leftrightarrow}}HB\)  
We derive the following statement by (Statement 22) and the belief rule:  
\(HB|\equiv P|\equiv ID_{PAT}\)  
We derive the following statement by (Statement 23), \(A16\), and the jurisdiction rule:  
\(HB|\equiv ID_{PAT}\)  
The patient \(P\) authenticates hospital B \(HB\). We derive the following statement by \(M4\) and the seeing rule:  
\(P\triangleleft(<ID_{HPB},R_{HPB},T_{HPB}>_{PK_{PAT}}<H(SEK_{BP},T_{PAT2})>_{ CHK_{PB}})\) (Statement 25)  
We derive the following statement by \(A9\) and the freshness rule:  
\(P|\equiv\#(<ID_{HPB},R_{HPB},T_{HPB}>_{PK_{PAT}}<H(SEK_{BP},T_{PAT2})>_{ CHK_{PB}})\) (Statement 26)  
We derive the following statement by (Statement 25), \(A11\), and the message meaning rule:  
\(P|\equiv HB|\sim(<ID_{HPB},R_{HPB},T_{HPB}>_{PK_{PAT}}<H(SEK_{BP},T_{PAT2})>_{ CHK_{PB}})\) (Statement 27)  
We derive the following statement by (Statement 26), (Statement 27), and the nonce verification rule:  
\(P|\equiv HB|\equiv(<ID_{HPB},R_{HPB},T_{HPB}>_{PK_{PAT}}<H(SEK_{BP},T_{PAT2})>_{ CHK_{PB}})\) (Statement 28)  
We derive the following statement by (Statement 28) and the belief rule:  
\(P|\equiv HB|\equiv P\stackrel{{\text{SEK}_{BP}}}{{ \leftrightarrow}}HB\)  
We derive the following statement by (Statement 29), \(A13\), and the jurisdiction rule:  
\(P|\equiv P\stackrel{{\text{SEK}_{BP}}}{{ \leftrightarrow}}HB\)  
We derive the following statement by (Statement 30) and the belief rule:  
\(P|\equiv HB|\equiv ID_{HPB}\)  
We derive the following statement by (Statement 31), \(A15\), and the jurisdiction rule:  
\(P|\equiv ID_{HPB}\)  
The hospital A \(HA\) authenticates the hospital B \(HB\).