## 4 Security Analysis of BSNCare+  
In this section, we analyze the security robustness of the major communication procedures of BSNCare+ and, based on the analyses, we have indicated that the BSNCare+ can achieve the principal security requirements as follows:  
* Claim 1: Mutual authentication can be achieved among communication entities in the BSNCare+. The mutual authentication of the BSNCare+ system is proven through BAN logic analysis [11]. Before the analysis, we present the basic constructs and logic postulates, where the symbols \(P\) and \(Q\) range over principals, \(X\) and \(Y\) range over statements, and \(K\) ranges over long-term secrets keys. All the symbols and abbreviations are presented in Table 2. \begin{table}
\begin{tabular}{c l} \hline \hline
**Symbol** & **Definition** \\ \hline \(P\), \(Q\) & Principals \\ \(X\), \(Y\) & Statements \\ \(K\) & Long-term secrets key or secrets \\ \(P\) believes \(X\) & The principal \(P\) believes that \(X\) is true \\ \(P\) sees \(X\) & Someone has sent a message containing \(X\) to \(P\), who can read and repeat \(X\) (possibly after doing some decryption) \\ \(P\) said \(X\) & \(P\) has sent a message containing statement \(X\) in the current session of the protocol or before \\ \(P\) controls \(X\) & \(P\) has jurisdiction over \(X\), i.e., the principal \(P\) is an authority on \(X\) and this matter should be trusted \\ fresh(\(X\)) & \(X\) has not been sent in a message before the current session of the protocol \\ \(P_{i}^{\text{F}}Q\) & The key \(K\) is shared between the principals \(P\) and \(Q\) \\ \([X]_{K}\) & This symbol represents the formula \(X\) encrypted or protected under the key \(K\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Basic constructs utilized in the analysis of Claim 1. Rule 1 (the message-meaning rules): If \(P\) believes \(P\overset{K}{\bigcirc}Q\) and \(P\) sees \(\{X\}_{K}\), then we postulate \(P\) believes \(Q\) said \(X\). Rule 2 (the nonce-verification rule): If \(P\) believes fresh(\(X\)) and \(P\) believes \(Q\) said \(X\), then we postulate \(P\) believes \(Q\) believes \(X\). Rule 3 (the jurisdiction rule): If \(P\) believes \(Q\) controls \(X\) and \(P\) believes \(Q\) believes \(X\), then we postulate \(P\) believes \(X\). Rule 4: If \(P\) sees (\(X\), \(Y\)) then \(P\) sees \(X\). In addition, if \(P\) believes \(P\overset{X}{\bigcirc}Q\) and \(P\) sees \(\{X\}_{K}\), then \(P\) sees \(X\). Rule 5: If one part of a formula is fresh, then the entire formula must also be fresh. If \(P\) believes fresh(\(X\)), then \(P\) believes fresh (\(X\), \(Y\)). Before we analyze the authentication process of the BSNCare+, the assumptions are given. \(\bigcirc\) Assumption 1: \(BS_{i}\) and _Server_ believe \(BS_{i}\)\(\overset{ID_{i}}{\leftrightarrow}\)\(\overset{K_{is}}{\leftrightarrow}\)\(\overset{ID_{sap}}{\leftrightarrow}\)_Server_  
Assumption 2: \(MG_{j}\) and _Server_ believe \(MG_{j}\)\(\overset{ID_{j}}{\leftrightarrow}\)\(\overset{K_{is}}{\leftrightarrow}\)_Server_  
Assumption 3: _Server_ believes fresh (\(N_{i}\), \(N_{j}\))  
Assumption 4: \(BS_{i}\) and \(MG_{j}\) believe fresh (\(N_{s1}\), \(N_{s2}\))  
Assumption 5: _Server_ believes \(BS_{i}\) controls (\(N_{i}\))  
Assumption 6: _Server_ believes \(MG_{j}\) controls (\(N_{j}\))  
Assumption 7: \(BS_{i}\) and \(MG_{j}\) believe _Server_ controls (\(N_{s1}\), \(N_{s2}\))  
The concrete realization of the authentication procedures of the BSNCare+ is presented as follows. Please refer to Table 1 for the definition of each symbol and Figure 1 for the detailed communication procedures of the BSNCare+. \(\bigcirc\) Step 1, \(BS_{i}\)\(\to\)\(MG_{j}\); \(MA_{A_{1}}\) = \(\{AID_{i}\), \(M_{1}\), \(N_{i}\), \(Tr_{seq}\) (if req. ), \(ID_{j}\), \(GPS_{j}\)}, where \(M_{1}\) = \(H\)(\(K_{is}\)\(\oplus\)\(N_{i}\))\(\oplus\)\(GPS_{i}\) and \(AID_{i}\) = \(H\)(\(M_{1}\)\(\mid\)\(GPS_{i}\)\(\mid\)\(1\)\(ID_{j}\)\(\mid\)\(GPS_{j}\)\(\mid\)\(1\)\(\it{Tr_{seq}\)}.