Formal Verification of Access Control Protocols in Distributed Systems - A Zero Trust Verification Framework

Abstract

Verifying protocols in quantum computing platforms requires rigorous analysis to ensure that security properties are correctly enforced. This thesis utilizes formal techniques to verify the access control protocols of quantum computing platform. The formal abstraction models capture key security properties, including authentication correspondence, chain integrity, proper token provenance, and defense-in-depth mechanisms. Verification results determine validity of critical protocol properties and unveil potential vulnerability in the system. The discussed methodology demonstrates the possibility of protocol interaction modeling despite stateful operations complexity in job management. The thesis presents a systematic verification framework for quantum platform access control, reconciling protocol functionality with security, while balancing model fidelity and verification tractability. The outcomes assist in strengthening the security foundations of quantum computing services by providing formally verified protocol implementations that uphold Zero Trust principles.