## 4 Security Analysis of BSNCare+
Step 2, \(MG_{j}\)\(\rightarrow\)_Server_: \(M_{A_{2}}\) =\(\{M_{2}\),\(N_{j}\),\(ID_{j}\),\(V_{1}\),\(M_{A_{1}}\)}, where \(M_{2}\) = \(H\)(\(K_{js}\)\(\oplus\)\(N_{j}\)) and \(V_{1}\) = \(H\)(\(M_{A_{1}}\)\(\mid\)\(Tr_{seq}\)\(\mid\)\(1\)\(ID_{j}\)\(\mid\)\(\mid\)\(N_{j}\)\(\mid\)\(K_{js}\)) and \(M_{A}\) = \(\{AID_{i}\), \(M_{1}\), \(N_{i}\), \(Tr_{seq}\) (if req. ), \(ID_{j}\), \(GPS_{j}\)}. Step 3, _Server_\(\rightarrow\)\(MG_{j}\):\(M_{A_{3}}\) = \(\{N_{s2}\), \(Tr\), \(V_{3}\), \(V_{2}\)}, where \(Tr\) = \(H\)(\(K_{is}\)\(\mid\)\(1\)\(N_{s2}\))\(\oplus\)\(Tr_{seq_{new}}\), \(V_{3}\) = \(H\)(\(Tr\)\(\mid\)\(K_{is}\)), \(V_{2}\) = \(H\)(\(ID_{j}\)\(\mid\)\(N_{s2}\)\(\mid\)\(K_{js}\)). Step 4, \(MG_{j}\)\(\rightarrow\)\(BS_{i}\): \(M_{A_{4}}\) = \(\{N_{s2}\), \(Tr\), \(V_{3}\)}, where \(Tr\) = \(H\)(\(K_{is}\)\(\mid\)\(N_{s2}\))\(\oplus\)\(Tr_{seq_{new}}\) and \(V_{3}\) = \(H\)(\(Tr\)\(\mid\)\(K_{is}\)). The formal analysis of mutual authentication of the BSNCare+ is demonstrated in the following. \(\bigcirc\) (1) \(MG_{j}\) sees \(M_{A_{3}}\) = \(\{N_{s2}\), \(Tr\), \(V_{3}\), \(V_{2}\}\): Based on Step 3, it is obvious that \(MG_{j}\) has received and seen \(M_{A_{3}}\) = \(\{N_{s2}\), \(Tr\), \(V_{3}\), \(V_{2}\}\). \(\bigcirc\) (2) \([PERSON]_{j}\) believes \(MG_{j}\)\(\overset{ID_{j}}{\leftrightarrow}\)_Server_: With the assumption 2, \(MG_{j}\) believes that it actually shares \(ID_{j}\) and \(K_{js}\) with the _Server_. \(\bigcirc\) (3) \([PERSON]_{j}\) believes _Server_ said \(\{V_{2}\}\): Based on the above two results, i.e., (1) and (2), we can derive that \([PERSON]_{j}\) believes _Server_ said \(\{V_{2}\}\) via Rule 1 (the message-meaning rules). \(\bigcirc\) (4) \([PERSON]_{j}\) believes fresh (\(N_{j}\)): As the \(N_{j}\) is issued by the \([PERSON]_{j}\) itself, \([PERSON]_{j}\) can tell the freshness of \(N_{j}\), and believes fresh (\(N_{j}\)) if it is. \(\bigcirc\) (5) \([PERSON]_{j}\) believes _Server_ believes \(\{V_{2}\}\): Based on the results (3) and (4), the fact of \([PERSON]_{j}\) believing that the _Server_ believes \(\{V_{2}\}\) is confirmed because Rule 2 (the nonce-verification rule) support this claim. \(\bigcirc\) (6) \([PERSON]_{j}\) believes _Server_ controls \(\{N_{s2}\}\): Based on the assumption 7, \(MG_{j}\) believes _Server_ actually controls the random number \(N_{s2}\). (7) \(MG_{j}\) believes \(\{V_{2}\}\): With the results (5) & (6) and Rule 3 (the jurisdiction rule), we can derive that \(MG_{j}\) believes \(\{V_{2}\}\). (8) \(BS_{i}\) sees \(M_{A_{4}}=\{N_{g2},\,\,Tr,\,V_{3}\}\)): With Step 4, \(BS_{i}\) has actually seen \(M_{A_{4}}=\{N_{g2},\,\,Tr,\,V_{3}\}\). (9) \(BS_{i}\) believes \(BS_{i}\)\(\stackrel{{ ID_{i},\,\,K_{is},\,\,SID,\,\,Tr_{seq}}}{{ \leftrightarrow}}\)_Server_: Based on the assumption 1, \(BS_{i}\) believes that it actually shares \(ID_{i},\,\,K_{is},\,\,SID\) and \(Tr_{seq}\) with the _Server_. (10) \(BS_{i}\) believes _Server_ said \(\{Tr,V_{3}\}\): Based on the above two results (8) and (9), we can derive that \(BS_{i}\) believes _Server_ said \(\{Tr,V_{3}\}\) via Rule 1 (the message-meaning rules). (11) \(BS_{i}\) believes fresh (\(N_{s2}\)): Based on the assumption 4, \(BS_{i}\) believes the freshness of \(N_{s2}\). (12) \(BS_{i}\) believes _Server_ believes \(\{Tr,\,\,V_{3}\}\): Based on the results (10) and (11), it is guaranteed that \(BS_{i}\) believes _Server_ believes \(\{Tr,\,\,V_{3}\}\) since Rule 2 (the nonce-verification rule). (13) \(BS_{i}\) believes _Server_ controls \(\{N_{s2}\}\): Based on the assumption 7, \(BS_{i}\) believes _Server_ actually controls the random number \(N_{s2}\). (14) \(BS_{i}\) believes \(\{Tr,\,\,V_{3}\}\): With the results (12) & (13) and Rule 3 (the jurisdiction rule), we can derive that \(BS_{i}\) believes \(\{Tr,\,\,V_{3}\}\).