2008/05/30 by Avik Chaudhuri, Chaudhuri, Avik
Computer Science · Social Sciences · #Access Control and Trust #Cryptography and Data Security #Cryptography and Security (cs.CR) #Distributed #FOS: Computer and information sciences #Parallel #Security and Verification in Computing #and Cluster Computing (cs.DC) #cs.CR #cs.DC
paper · pdf · doi:10.48550/arxiv.0805.4665
arxiv created 2008/05/30 · openalex publication_date 2008/05/30 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Distributed implementations of access control abound in distributed storage protocols. While such implementations are often accompanied by informal justifications of their correctness, our formal analysis reveals that their correctness can be tricky. In particular, we discover several subtleties in a standard protocol based on capabilities, that can break security under a simple specification of access control. At the same time, we show a sensible refinement of the specification for which a secure implementation of access control is possible. Our models and proofs are formalized in the applied pi calculus, following some new techniques that may be of independent interest. Finally, we indicate how our principles can be applied to securely distribute other state machines.