This thesis presents a formal model and protocol of a specific cloud-based Key Management Service (KMS) for the purpose of design validation.. The KMS architecture, inspired by industry-leading implementations, employs a layered structure facilitating envelope encryption. The study addresses whether this specific design can be formalized and validated using formal methods and associated tools. An abstract protocol defining the KMS operations was devised, which specified synchronized component classes and assumptions regarding, among other things, cryptography, databases, and scheduling. After exploring different formal approaches, the Spin model checker was chosen to verify the KMS. Four Promela models were created, each exhibiting different protocol operations with two tenants as initiators, allowing observation of concurrent protocol execution. Linear Temporal Logic (LTL) specifications were crafted to validate desired behaviors related to functional requirements. The safety specification focused on secure key management and correct message sequencing, while the liveness specifications for each model confirmed correct handling of all incoming requests. The verification process successfully validated several functional aspects of the KMS, demonstrating the feasibility of using model checking to verify security properties from a functional standpoint. However, it also highlighted the challenges in capturing the full complexity of such a service within model checking constraints. This work provides a foundation for further verification efforts for the KMS, suggesting areas for protocol refinement and more comprehensive modeling of complex KMS aspects like error handling, node failure recovery, and cryptographic operations in distributed settings.

Denna avhandling presenterar en formell modell och ett protocol av en molnbaserad Key Management Service (KMS), med avsikt att validera designen. KMS-arkitekturen, inspirerad av branschledande implementationer, är strukturerad i olika lager, vilket underlättar envelope encryption. Studien undersöker om denna specifika design kan formaliseras och valideras med hjälp av formella metoder och relaterade verktyg. Ett abstrakt protokoll som definierar KMS-operationerna utformades, där synkroniserade kompo- nentklasser och antaganden kring, bland annat, kryptografi, databaser och schemaläggning av processer specificerades. Efter att ha utforskat olika formella metoder valdes Spin model checker för att verifiera KMSen. Fyra Promela-modeller skapades, där varje modell representerade olika protokolloperationer med två klienter som initierare, vilket möjliggjorde observation av samtidiga exekevringar av protokollet. Specifikationer i linjär temporallogik (LTL) utformades för att validera önskade beteenden relaterade till funktionella krav. Safety specifikationen fokuserade på säker nyckelhan- tering och korrekta meddelandesekvenser, medan liveness specifikationerna för vardera modell bekräftade korrekt hantering av samtliga inkommande requests. Verifieringsprocessen validerade framgångsrikt flera funktionella aspekter av KMSen, vilket visade att det är möjligt att använda model checking för att verifiera säkerhetsegenskaper ur ett funktionellt perspektiv. Det framhävde dock även utmaningarna i att fånga den övergripande komplexiteten hos en sådan tjänst, inom begränsningarna för model checking. Detta arbete utgör en grund för vidare verifieringsinsatser av KMSen och föreslår områden för protokollförfining och mer omfattande modellering av komplexa KMS- aspekter såsom felhantering, återhämtning från nodfel och kryptografiska operationer i distribuerade miljöer.