## 3 Simple Resource Algorithm
### Advertising Cloud Formulation
CB \(\rightarrow\) SA: aenc((Ns, Nc, CB), pkS)

Figure 4: Migration between SA to CB. \begin{table}
\begin{tabular}{c c} \hline \hline
**Notation** & **Explanation** \\ \hline CA, CB, SA and SB & Cloud and Server Identities \\ pkC/skC, pkS/skS, pkR/skR & public and private key pairs of Cloud CB, \\ Server SA \& Registry \\ M\_Reqc, M\_Trfs, M\_Ackc & Request for migration, transfers and acknowledgement \\ sign & Signature/signed by the Registry \\ aenc & Asymmetric Encryption \\ enc & Symmetric Encryption \\ Ksc & Symmetric session key \\ Ns, Nc & Nonce of SA and CB \\ ResSA, ResCB & Requested Resources of SA \& CB \\ \hline \hline \end{tabular}
\end{table} 
Table 2: RASP Table. 3. **Stage 3: Migration transfer**: In Step 8, Server SA generates the session key (Ksc) to start the migration. In Step 9, Cloud CB sends the migration initialization request. In Step 10, Server SA performs the migration transfer. In Step 11, Cloud CB sends an acknowledgment to Server SA. 8. SA \(\rightarrow\) CB: aenc((Nc, Ksc), pkC) 9. CB \(\rightarrow\) SA: enc ((M_Reqc, SA), Ksc) 10. SA \(\rightarrow\) CB: enc ((M_Trfs, ResSA), Ksc) 11. CB \(\rightarrow\) SA: enc ((M_Ackc), Ksc)
4. **Stage 4: Update of New service location to the Registry**: In Step 12, the service on Cloud CB (SB) updates the Registry on its new location. The new service SB is now running on Cloud CB and informs the Registry that it has been successfully migrated. 12. SB \(\rightarrow\) R: aenc((SB, CB), pkR)

### ProVerif an Overview

ProVerif [12] is a formal verification and highly automated tool used for analyzing the security properties of cryptographic protocols. It employs applied calculus to model concurrent systems and their interactions. The tool comprehends the protocol's abstraction, including how messages are exchanged between parties and the use of cryptographic primitives such as encryption, decryption, and signatures. ProVerif verifies the service migration mechanism's secrecy, authentication, and key exchange. Another strength of this tool is that it performs symbolic analysis, aiding in understanding attack scenarios. ProVerif provides attack traces [13] if it finds any violations of a security property. The output of the Query attacker() query function results as \"True\", indicating that the security property cannot be accessed by the attacker. This validates the attacker's lack of knowledge and ensures the secrecy of data authentication between parties or multiple roles for securely transferring data and authenticated across an unlimited number of sessions using unbounded data. If the outcome of the attacker() function is \"False\", the security property value is accessible to the attacker. Finally, the result displays any attack trace and indicates whether the attacker() query returns TRUE or FALSE. ProVerif Results

The results shown in Table 3 indicate that RASP can preserve the secrecy, authentication and key exchange of the service migration mechanism. * **Nonces are secured and not derived by the attacker:** specific nonces (SNs, SNc, CNs, CNc) used in the protocol are not derivable by an attacker, ensuring their confidentiality. Each line indicates that the respective nonce cannot be compromised (is true). * **Session key:** Results confirm that the session key (Ksc) and associated bitstrings (SNk, CNk) are secure from the attacker. The line \"RESULT not attacker_bitstring (SNk []) is true\" with Ksc also specifies the conditions under which this key is secure. * **Private keys:** Results confirm that the session key (Ksc) and associated bitstrings (SNk, CNk) are secure from the attacker. The line \"RESULT not attacker_bitstring (CNk []) is true\" with Ksc also specifies the conditions under which this key is secure. * **Authentication:** It validates the mutual authentication between SA and CB. The use of inj-event indicates that the protocol verifies injective correspondence, meaning each event endSparam (or endCparam) has a matching beginSparam (or beginCparam), ensuring that both parties authenticate each other correctly.