Formal Analysis of Dynamic, Distributed File-System Access Controls

Avik Chaudhuri and Martín Abadi

We 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. We establish that the networked storage systems implement simpler, centralized storage specifications with local access-control checks. More specifically, we prove that the former systems preserve safety properties of the latter systems. Focusing on security, we then derive strong secrecy and integrity guarantees for the networked storage systems.


    author = {Avik Chaudhuri and Mart\'{\i}n Abadi},
    title = {Formal Analysis of Dynamic, Distributed File-System Access Controls},
    booktitle = {Proceedings of the 26th IFIP WG6.1 International Conference on
                 Formal Techniques for Networked and Distributed Systems (FORTE'06)},
    year = {2006},
    pages = {99-114},
    publisher = {Springer},
    year = {2006}