## 5 Formal Modeling and Analysis of SAPS  
We have performed formal modeling using a method known as Nonmonotonic Cryptographic Protocol (NCP), also called Rubin Logic [39]. The analysis verification of the SAPS protocol is as per its previous terms and specification of NCP. NCP authenticates the proposed scheme as per the regular necessities of cryptographic procedures, considering parameters such as authenticity, data integrity, the freshness of received data, message encryption, and decryption, etc. This will also help identify the lack of certain properties in the presented scheme and for potential data compromising scenarios. This analysis is similar to the actual operation functionalities in a programming scenario. When we talk about Rubin Logic, the units are assigned specific roles, and a universal set of information is maintained. It also maintains current state of the parameters of users after each update operation. Global sets are accessible to all the member nodes and can be categorized into four types which are secret, observer, rule, and first sets. A detailed discussion of the formal specification for WSAN protocols is provided in [26; 29], along with appropriate case studies. Entity or node contains a local set that can be categorized into ownership, represented as POSS (), a set of beliefs known as belief BEL (), and to represent the behavior, set BL (). Detailed specification of these sets can be explored in [14; 30]. Table 2 represents the local set for the application scenario of Rubin logic on SAPS-AN. The details of SAPS, its verification, and analysis provide a detailed overview of all sets maintained under the category of the local set. All the participating entities, including sender, receiver, and Trusted Server are separately maintained locally. An ownership set, POSS (entity), contains all the  
Figure 3: Secure authentication and prescription safety protocol steps. parameters involved in encryption, decryption, and other processes accomplished in a local memory of each entity, as described in the section below. For the operations and input arguments that are performed in implementation steps, a Behavior List BL () is maintained. Local sets for the entities of the Trusted Server (TS), patient (A) as first party, and Doctor (B) as the second party are presented in Tables 2-4, respectively. \begin{table}
\begin{tabular}{l} \hline \hline \(\text{POSS}(\text{A})=\{\text{ID}_{\text{A}},\text{P},\text{R}_{\text{P}},\text {K}_{\text{A-TS}},\text{F},\text{PW}_{\text{P}}\}\) \\ \(\text{BEL}(\text{A})=\{\#(\text{ID}_{\text{A}}),\#(\text{P}),\#(\text{R}_{\text{P}}), \#(\text{K}_{\text{A-TS}}),\#(\text{F}),\#(\text{PW}_{\text{P}})\}\) \\ \(\text{IM}(\text{R}_{\text{P}},\text{P})\to\text{X}_{\text{A}},\text{Mul}\ (\text{R}_{\text{P}},\text{F})\to\text{Y}_{\text{A}}\) \\ \(\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{Concat}(\text{ID}_{\text{A}},\text{M}_{\text{A}},\text{N}_{\text{I}}, \text{MAC}(\text{M}_{\text{A}}),\text{ID}_{\text{B}})\to\text{Q}_{\text{A}}\) \\ \(\text{Hash}(\text{h},\text{:})\text{Y}_{\text{A}}\to\text{H}_{\text{YA}}\) \\ \(\text{Encrypt}(\text{[Q}_{\text{A}},\text{H}_{\text{YA}})]\to\text{P}_{\text{A}}\) \\ \(\text{Encrypt}(\text{[C}_{\text{OCT}}(\text{X}_{\text{A}},\text{P}_{\text{A}}, \text{T}_{1}),\text{K}_{(\text{A-TS})})\to\text{C}_{\text{A}}\) \\ \(\text{Hash}(\text{h},\text{:})\text{Concat}(\text{X}_{\text{A}},\text{P}_{\text{A}}, \text{N}_{\text{I}})\to\text{ID}_{\text{A-T}}\) \\ \(\text{Send}(\text{(ID}_{\text{A-T}},\text{C}_{\text{A}}))\) to TS and Update (ID\({}_{\text{A-T}}\)) \\ Receive(TS, (CP\({}_{\text{A}}\))) \\ Decrypt(\(\text{[ID}_{\text{TS}},\text{CP}_{\text{A}}]\)) \\ Hash(\(\text{h},\text{:})\text{Concat}(\text{dX}_{\text{B}},\text{ID}_{\text{B}}, \text{ID}_{\text{A}})\to\text{S}_{\text{KA}}\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Local set at (Patient) (A).