## 5 Formal Modeling and Analysis of SAPS
### SAPS Analysis and Verification
\begin{table}
\begin{tabular}{l} \hline \hline \(\text{POSS(B)}\) = (ID\({}_{\text{B}}\), P, R\({}_{\text{B-TS}}\), F, PW\({}_{\text{B}}\)) \\ BEL(A) = \(\{\#(ID\({}_{\text{B}}\)), \#(P), \#(R\({}_{\text{B}}\)), \#(K\({}_{\text{(B-TS)}}\)), \#(F), \#(PW\({}_{\text{B}}\))] \\ BL(A) = \\ Receive(TS, [C\({}_{\text{TS}}\)]) \\ Decrypt([ID\({}_{\text{B-T}}\), \({}_{\text{TS}}\)]K\({}_{\text{B-TS}}\)) and Split to get [ID\({}_{\text{A}}\), Z\({}_{\text{TS}}\), T\({}_{2}\), N\({}_{2}\)] \\ Hash(h(.); Concat(ID\({}_{\text{A}}\), ID\({}_{\text{B}}\), N\({}_{\text{2}}\)) \(\rightarrow\) Q\({}^{\prime}\)T\({}_{\text{S}}\) \\ check(XOR(Z\({}_{\text{TS}}\), Q\({}_{\text{TS}}\))! equals ID\({}_{\text{B-T}}\)) then abort \\ Mul (R\({}_{\text{B}}\), P) \(\rightarrow\) X\({}_{\text{B}}\), Mul (R\({}_{\text{B}}\), F) \(\rightarrow\) Y\({}_{\text{B}}\) \\ Hash(h(.); Concat(PW\({}_{\text{B}}\), ID\({}_{\text{TS}}\), ID\({}_{\text{B}}\))) \(\rightarrow\) M\({}_{\text{B}}\) \\ Concat(ID\({}_{\text{B}}\), M\({}_{\text{B}}\), N\({}_{\text{A}}\), MAC(M\({}_{\text{B}}\)), ID\({}_{\text{TS}}\)) \(\rightarrow\) Q\({}_{\text{B}}\) \\ Hash(h(.); Y\({}_{\text{B}}\)) \(\rightarrow\) H\({}_{\text{P}}\) \\ Encrypt([Q\({}_{\text{B}}\), H\({}_{\text{P}}\)]) \(\rightarrow\) P\({}_{\text{B}}\) \\ Encrypt([Concat(X\({}_{\text{B}}\), P\({}_{\text{B}}\),T\({}_{3}\)),K\({}_{\text{(B-TS)}}\)]) \(\rightarrow\) C\({}_{\text{B}}\) \\ Send((ID\({}_{\text{B-T}}\), C\({}_{\text{B}}\))) to TS and Update(ID\({}_{\text{B-T}}\)) \\ \hline Receive(TS, [C\({}_{\text{P}}\)]) \\ Decrypt([ID\({}_{\text{TS}}\), CP\({}_{\text{B}}\)]) H\({}_{\text{P}}\)) and Split to get [X\({}_{\text{A}}\), ID\({}_{\text{A}}\), ID\({}_{\text{B}}\), Y\({}^{\prime}\)B, N\({}_{\text{2}}\)] \\ Hash(h(.); Concat(dX\({}_{\text{A}}\), ID\({}_{\text{B}}\), ID\({}_{\text{A}}\))) \(\rightarrow\) S\({}_{\text{AB}}\) \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Local set at Patient/Doctor (B). \(\bullet\)Hash(h(. ); Concat(PW\({}_{\text{P}}\), ID\({}_{\text{A}}\), ID\({}_{\text{B}}\))) \(\rightarrow\) M\({}^{{}^{\prime}}\)\({}_{\text{A}}\)  
\(\bullet\)if MAC(M\({}^{{}^{\prime}}\)\({}_{\text{A}}\)) equals MAC(M\({}_{\text{A}}\)) else discard  
\(\bullet\)if M\({}^{{}^{\prime}}\)\({}_{\text{A}}\) NOT equals M\({}_{\text{A}}\) then discard  
After Patient (A) verification, the TS calculates some parameters and generates a message for the other party that can provide medical services to the patient (A) as follows. \(\bullet\)Hash(h(. ); Concat(IDTS, IDB, RTS)) \(\rightarrow\) ZTS  
\(\bullet\)Hash(h(. ); Concat(IDA, IDB, N2)) \(\rightarrow\) QTS  
\(\bullet\)XOR(ZTS, QTS) \(\rightarrow\) IDB- T  
\(\bullet\)Encrypt((Concat (IDA, ZTS, T2, N2, IDB-T), K(TS-B))) \(\rightarrow\) CTS  
\(\bullet\)Send((IDTS, CTS)) to B and Update (IDB- T)  
Upon receiving the secret credentials sent by the TS, Doctor (B) verifies the message integrity and the TS as follows:  
\(\bullet\)Decrypt((IDB-T, CTS)KBT-TS) and Split to get [IDA, ZTS, T2, N2]  
\(\bullet\)Hash(h(. ); Concat (IDA, IDB, N2)) \(\rightarrow\) Q\({}^{\prime}\)\({}_{\text{TS}}\)  
\(\bullet\)check(XOR(ZTS,Q\({}^{\prime}\)**TS**)! equals IDB-T) then abort  
Following the authentication and verification of Party (B) by the TS, party (B) also computes some secret credentials and provides a reply message for the TS. The secret credentials are used by both parties to generate a secret key, and the transmission is secured using the shared key, as well as by calculating the hash, adding a nonce, and MAC. The steps performed at the physician's side for session key establishing are as follows:  
\(\bullet\)Mul(R\({}_{\text{B}}\), P) \(\rightarrow\) X\({}_{\text{B}}\), Mul(R\({}_{\text{B}}\), F) \(\rightarrow\) Y\({}_{\text{B}}\)  
\(\bullet\)Hash(h(. ); Concat (P\({}_{\text{WB}}\), ID\({}_{\text{TS}}\), ID\({}_{\text{B}}\))) \(\rightarrow\) M\({}_{\text{B}}\)  
\(\bullet\)Concat(IDB,M\({}_{\text{B}}\), N\({}_{\text{A}}\), MAC(M\({}_{\text{B}}\)), ID\({}_{\text{TS}}\)) \(\rightarrow\) Q\({}_{\text{B}}\)  
\(\bullet\)Hash(h(.