## 5 Formal Modeling and Analysis of SAPS
\begin{table}
\begin{tabular}{l} \hline \hline \(\text{POSS}(\text{T}_{\text{S}})=\{\text{ID}_{\text{TS}},\text{K}_{\text{(TS -Al)}},\text{K}_{\text{(TS -B)}}\}\) \\ \(\text{BEL}(\text{T}_{\text{S}})=\{\#(\text{ID}_{\text{TS}}),\#(\text{K}_{\text{(TS -Al)}},\#\text{K}_{\text{(TS -B)}}\}\) \\ \(\text{BL}(\text{T}_{\text{S}})=\{A,\text{C}_{\text{A}}\})\) \\ \(\text{Decrypt}(\text{[ID}_{\text{A-T}},\text{C}_{\text{A}}])\) \\ \(\text{check}(\text{[X}^{\text{T}}_{\text{1}}\text{-T})\geq\Delta\Gamma\) then abort \\ \(\text{Hash}(\text{h},\text{:})\text{Mul}(\text{d},\text{X}_{\text{A}}))\to\text{H}_{ \text{YA}}\) \\ \(\text{Decrypt}(\text{[PA}_{\text{A}}\text{H}_{\text{YA}}))\) and Split to get \(\text{[ID}_{\text{A}},\text{M}_{\text{A}},\text{N}_{\text{I}},\text{MAC}( \text{M}_{\text{A}}),\text{ID}_{\text{B}}]\) \\ \(\text{Hash}(\text{h},\text{:})\text{Concat}(\text{PW}_{\text{P}},\text{ID}_{ \text{A}},\text{ID}_{\text{B}})\to\text{M}_{\text{A}}\) \\ \(\text{if MAC}(\text{A}\)) equals MAC(M\(\text{A}_{\text{A}})\) else discard \\ if MAC(M\(\text{A}\)) equals MAC(M\(\text{A}_{\text{A}})\) else discard \\ if MAC output \(\text{M}_{\text{A}}\) then discard \\ \hline \hline \(\text{Hash}(\text{h},\text{:})\text{Concat}(\text{ID}_{\text{B}},\text{ID}_{ \text{B}},\text{R}_{\text{TS}}))\to\text{Z}_{\text{TS}}\) \\ \(\text{Hash}(\text{h},\text{:})\text{Concat}(\text{ID}_{\text{A}},\text{ID}_{ \text{B}},\text{N}_{\text{I}}))\to\text{Q}_{\text{TS}}\) \\ \(\text{XOR}\)\((\text{Z}_{\text{TS}},\text{Q}_{\text{TS}})\to\text{ID}_{\text{B-T}}\) \\ \(\text{Encrypt}(\text{[C}_{\text{OCT}}(\text{ID}_{\text{A}},\text{Z}_{\text{TS}}, \text{T}_{\text{2}},\text{N}_{\text{2}},\text{ID}_{\text{B-T}}),\text{K}_{ \text{(TS-B)}}))\to\text{C}_{\text{TS}}\) \\ \(\text{Send}(\text{(ID}_{\text{TS}},\text{C}_{\text{TS}}))\) to B and Update (ID\({}_{\text{B-T}}\)) \\ \hline \hline \(\text{Receive}(\text{B},\text{[C}_{\text{B}}])\) \\ \(\text{Derypt}(\text{[ID}_{\text{B-T}},\text{C}_{\text{B}}|\text{K}_{\text{TS -B}}))\) and Split to get \(\text{[X}_{\text{B}},\text{P}_{\text{B}},\text{T}_{\text{3}}]\) \\ \(\text{check}(\text{[T}_{\text{3}}\text{-T})\geq\Delta\Gamma\) then abort \\ \(\text{Hash}(\text{h},\text{:})\text{Mul}(\text{d},\text{X}_{\text{B}}))\to\text{H}_{ \text{YB}}\) \\ \(\text{Decrypt}(\text{[P}_{\text{B}}|\text{H}_{\text{Y}}\text{-B}]\) and Split to get \(\text{[ID}_{\text{B}},\text{M}_{\text{B}},\text{N}_{\text{I}},\text{MAC}( \text{M}_{\text{B}}),\text{ID}_{\text{TS}}]\) \\ \(\text{Hash}(\text{h},\text{:})\text{Concat}(\text{PW}_{\text{B}},\text{ID}_{ \text{S}},\text{ID}_{\text{B}}))\to\text{M}_{\text{B}}\) \\ \(\text{if MAC(M}\)\(\text{g}\) equals MAC(M\(\text{M}_{\text{B}})\) else discard \\ if M g is NOT equals Mg then discard \\ \hline \hline \(\text{Encrypt}(\text{[C}_{\text{OCT}}(\text{X}_{\text{B}},\text{ID}_{\text{A}}, \text{ID}_{\text{B}},\text{T}_{\text{A}},\text{N}_{\text{I}}),\text{H}_{ \text{Y}}\text{-A}))\to\text{CP}_{\text{A}}\) \\ \(\text{Send}(\text{(ID}_{\text{A-T}},\text{CP}_{\text{A}}))\) to A \\ \(\text{Encrypt}(\text{[Concat}(\text{X}_{\text{A}},\text{ID}_{\text{A}},\text{ID}_{ \text{B}},\text{Y}^{\text{P}}_{\text{B}},\text{N}_{\text{I}}),\text{H}_{ \text{Y}}\text{-B})\)\(\to\text{CP}_{\text{B}}\) \\ \(\text{Send}(\text{(ID}_{\text{B-T}},\text{CP}_{\text{B}}))\) to B \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Local Set at Trusted Server (TS).