Formal Analysis of Dynamic, Distributed File-System Access Controls

The authors model networked storage systems with distributed, cryptographically enforced file-access control in an applied pi calculus. The calculus contains cryptographic primitives and supports file-system constructs, including access revocation. They establish that the networked storage systems implement simpler, centralized storage specifications with local access-control checks. More specifically, the authors prove that the former systems preserve safety properties of the latter systems. Focusing on security, they then derive strong secrecy and integrity guarantees for the networked storage systems.