These resources are requested in the context of the WASP NEST Source project. A brief summary of the project follows: In the future, computing and communication systems must accommodate a diverse range of applications, including telemedicine, intelligent transportation, extended reality (XR), and personal assistants. Some of these are already a reality, thanks to powerful computer hardware, faster and more reliable mobile communication (such as 5G), and significant advancements in AI and software technologies. Notably, generative AI has made remarkable progress in recent years, unlocking numerous possibilities for research in this field. This project aims to leverage generative AI to address critical challenges related to secure resource allocation in dynamic edge scenarios. Researchers in this project will explore how to specify, train, and verify generative AI models for creating orchestration mechanisms and protocols. Their goals include detecting and mitigating attacks against intelligent Function as a Service (FaaS) systems and enabling runtime security verification for both manually and automatically generated orchestration mechanisms. An important part of the of the project is formal verification of cryptographic protocols using the Tamarin prover. Verification of such properties means trying to find counterexamples to first-order logic statements about possible runs of a given protocol. If the prover can establish that no such counterexample exists, then the property has been proven to hold. However, since there are many possible runs of a distributed protocol, the prover must go through all of them for the proof to hold. This requires substantial computational resources. In this proposal we only request ordinary CPU resources as this part of the project will not require AI/ML training. Such resources for Berzelius will probably be needed later on.