# A Blockchain-Based Secure Inter-Hospital EMR Sharing System
## 4 Security Analysis
### Mutual Authentication
We derive the following statement by \(M2\) and the seeing rule: \(P\triangleleft(<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{PAT}}<H(SEK_{AP},T_{PAT})>_{ CHK_{PA}})\) (Statement 9) We derive the following statement by (Statement 1) and the freshness rule: \(P\big{|}\equiv\#(<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{PAT}}<H(SEK_{AP},T_{PAT})>_{ CHK_{PA}})\) (Statement 10) We derive the following statement by (Statement 9), \(A3\), and the message meaning rule: \(P\big{|}\equiv HA\big{|}\sim(<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{PAT}}<H(SEK_{AP}, T_{PAT})>_{CHK_{PA}})\) (Statement 11) We derive the following statement by (Statement 10), (Statement 11), and the nonce verification rule: \(P\big{|}\equiv HA\big{|}\equiv(<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{PAT}}<H(SEK_{AP}, T_{PAT})>_{CHK_{PA}})\) (Statement 12) We derive the following statement by (Statement 12) and the belief rule: \(P\big{|}\equiv HA\big{|}\equiv P\stackrel{{ SEK_{AP}}}{{ \leftrightarrow}}HA\) (Statement 13) We derive the following statement by (Statement 13), \(A5\), and the jurisdiction rule: \(P\big{|}\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) (Statement 14) We derive the following statement by (Statement 14) and the belief rule: \(P\big{|}\equiv HA\big{|}\equiv ID_{HPA}\) (Statement 15) We derive the following statement by (Statement 15), \(A7\), and the jurisdiction rule: \(P\big{|}\equiv ID_{HPA}\) (Statement 16)  
By (Statement 6), (Statement 8), (Statement 14), and (Statement 16), it can be proven that, in the proposed scheme, the patient \(P\) and hospital A \(HA\) authenticate each other. Moreover, it can also be proven that the proposed scheme can establish a session key between the patient \(P\) and hospital A \(HA\). In the proposed scheme, hospital A authenticates the patient by  
\[CHK_{AP}\stackrel{{?}}{{=}}H_{3}(SEK_{AP},T_{HPA}).\]If it passes the verification, hospital A authenticates the legality of the patient. The patient authenticates hospital A by  
\[CHK_{PA}\stackrel{{?}}{{=}}H_{3}(SEK_{AP},T_{PAT}).\]  
If it passes the verification, the patient authenticates the legality of hospital A. The initial treatment authentication and communication phase of the proposed scheme thus guarantees mutual authentication between hospital A and the patient. In the inter-hospital 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 B \(HB\) and also between hospital B \(HB\) and hospital A \(HA\). \begin{tabular}{l l} \(G9\): & \(P|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(G10\): & \(P|\equiv HB|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(G11\): & \(HB|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(G12\): & \(HB|\equiv P|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HB\) \\ \(G13\): & \(P|\equiv ID_{HPB}\) \\ \(G14\): & \(P|\equiv HA|\equiv ID_{HPB}\) \\ \(G15\): & \(HB|\equiv ID_{PAT}\) \\ \(G16\): & \(HB|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G17\): & \(P|\equiv P\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G18\): & \(HB|\equiv HA|\equiv HB\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G19\): & \(HA|\equiv HB\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G20\): & \(HA|\equiv HB|\equiv HB\stackrel{{ SEK_{AP}}}{{\leftrightarrow}}HA\) \\ \(G21\): & \(HB|\equiv ID_{HPA}\) \\ \(G22\): & \(HB|\equiv HA|\equiv ID_{HPA}\) \\ \(G23\): & \(HA|\equiv ID_{HPB}\) \\ \(G24\): & \(HA|\equiv HB|\equiv ID_{HPB}\) \\ \end{tabular}   
According to the inter-hospital authentication and communication phase, BAN logic is applied in order to produce an idealized form as follows: \begin{tabular}{l l} \(M3\): & \((<ID_{PAT},R_{PAT},T_{PAT2}>_{PK_{H}m},<H(SEK_{BP},T_{HPB})>_{CHK_{BP}})\) \\ \(M4\): & \((<ID_{HPB},R_{HPB},T_{HPB}>_{PK_{PAT}},<H(SEK_{BP},T_{PAT2})>_{CHK_{RB}})\) \\ \(M5\): & \((<ID_{HPB},R_{HPB},T_{HPB2}>_{PK_{HPA}},<H(SEK_{AB},T_{HPA2})>_{CHK_{AB}})\) \\ \(M6\): & \((<ID_{HPA},R_{HPA},T_{HPA}>_{PK_{H}m},<H(SEK_{AB},T_{HPB2})>_{CHK_{BA}})\) \\ \end{tabular}