# A Blockchain-Based Secure Inter-Hospital EMR Sharing System
## 4 Security Analysis
### Mutual Authentication
We derive the following statement by \(M5\) and the seeing rule:  
\(HA\triangleleft(<ID_{HPB},R_{HPB},T_{HPB2}>_{PK_{HPA}}<H(SEK_{AB},T_{HPA2})>_{ CHK_{AB}})\) (Statement 33)  
We derive the following statement by \(A18\) and the freshness rule:  
\(HA|\equiv\#(<ID_{HPB},R_{HPB},T_{HPB2}>_{PK_{HPA}}<H(SEK_{AB},T_{HPA2})>_{ CHK_{AB}})\) (Statement 34)We derive the following statement by (Statement 33), \(A20\), and the message meaning rule:  
\(HA|\equiv HB|\sim(<ID_{HPB},R_{HPB},T_{HPB2}>_{PK_{HPA}},<H(SEK_{AB},T_{HPA2})>_{ CHK_{AB}})\) (Statement 35)  
We derive the following statement by (Statement 34), (Statement 35), and the nonce verification rule:  
\(HA|\equiv HB|\equiv(<ID_{HPB},R_{HPB},T_{HPB2}>_{PK_{HPA}},<H(SEK_{AB},T_{HPA2})>_{ CHK_{AB}})\) (Statement 36)  
We derive the following statement by (Statement 36) and the belief rule:  
\(HA|\equiv HB|\equiv HB\overset{SEK_{AB}}{\leftrightarrow}HA\) (Statement 37)  
We derive the following statement by (Statement 37), \(A22\), and the jurisdiction rule:  
\(HA|\equiv HB\overset{SEK_{AB}}{\leftrightarrow}HA\) (Statement 38)  
We derive the following statement by (Statement 38) and the belief rule:  
\(HA|\equiv HB|\equiv ID_{HPB}\) (Statement 39)  
We derive the following statement by (Statement 39), \(A24\), and the jurisdiction rule:  
\(HA|\equiv ID_{HPB}\) (Statement 40)  
The hospital B \(HB\) authenticates the hospital A \(HA\). We derive the following statement by \(M6\) and the seeing rule:  
\(HB\lhd\lhd(<ID_{HPA},R_{HPA},T_{HPA2}>_{PK_{HPB}},<H(SEK_{AB},T_{HPB2})>_{ CHK_{BA}})\) (Statement 41)  
We derive the following statement by \(A17\) and the freshness rule:  
\(HB|\equiv\#(<ID_{HPA},R_{HPA},T_{HPA2}>_{PK_{HPB}},<H(SEK_{AB},T_{HPB2})>_{ CHK_{BA}})\) (Statement 42)  
We derive the following statement by (Statement 41), \(A19\), and the message meaning rule:  
\(HB|\equiv HA|\sim(<ID_{HPA},R_{HPA},T_{HPA2}>_{PK_{HPB}},<H(SEK_{AB},T_{HPB2})>_{ CHK_{BA}})\) (Statement 43)  
We derive the following statement by (Statement 42), (Statement 43), and the nonce verification rule:  
\(HB|\equiv HA|\equiv(<ID_{HPA},R_{HPA},T_{HPA2}>_{PK_{HPB}},<H(SEK_{AB},T_{HPB2})>_{ CHK_{BA}})\) (Statement 44)  
We derive the following statement by (Statement 44) and the belief rule:  
\(HB|\equiv HA|\equiv HB\overset{SEK_{AB}}{\leftrightarrow}HA\) (Statement 45)  
We derive the following statement by (Statement 45), \(A21\), and the jurisdiction rule:  
\(HB|\equiv HB\overset{SEK_{AB}}{\leftrightarrow}HA\) (Statement 46)  
We derive the following statement by (Statement 46) and the belief rule:  
\(HB|\equiv HA|\equiv ID_{HPA}\) (Statement 47)  
We derive the following statement by (Statement 47), \(A23\), and the jurisdiction rule:  
\(HB|\equiv ID_{HPA}\) (Statement 48)  
By (Statement 22), (Statement 24), (Statement 30), and (Statement 32), it can be proven that, in the proposed scheme, the patient \(P\) and hospital B \(HB\) authenticate each other. Moreover, it can also be proven that the proposed scheme can establish a session key between the patient \(P\) and hospital B \(HB\). In the proposed scheme, hospital B authenticates the patient by  
\[CHK_{BP}\overset{?}{=}H_{3}(SEK_{BP},T_{HPB}).\]  
If it passes the verification, hospital B authenticates the legality of the patient. The patient authenticates hospital B by  
\[CHK_{PB}\overset{?}{=}H_{3}(SEK_{BP},T_{PAT2}).\]  
In the proposed scheme, hospital A authenticates the hospital B by  
\[CHK_{AB}\overset{?}{=}H_{3}(SEK_{AB},T_{HPA2}).\]If it passes the verification, hospital A authenticates the legality of hospital B. Hospital B authenticates the hospital A by  
\[CHK_{BA}\stackrel{{?}}{{=}}H_{3}(SEK_{AB},T_{HPB2}).\]  
If it passes the verification, hospital B authenticates the legality of hospital A. The inter-hospital authentication and communication phase of the proposed scheme thus guarantees mutual authentication between the patient, \(P\), and hospital B, \(HB\), and also between hospital B, \(HB\), and hospital A, \(HA\).