On Secure Distributed Implementations of Dynamic Access Control

Avik Chaudhuri

Abstract
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 natural 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.

PDF

BibTeX
@inproceedings{sdidac-C08,
    author = {Avik Chaudhuri},
    title = {On Secure Distributed Implementations of Dynamic Access Control.},
    booktitle = {Proceedings of the Joint Workshop on Foundations of Computer Security,
                 Automated Reasoning for Security Protocol Analysis,
                 and Issues in the Theory of Security (FCS-ARSPA-WITS'08)},
    year = {2008},
    pages = {93--107}
}

A longer version of this paper, containing proofs and other details, appears as UCSC Computing Research Laboratory Technical Report 08-01, and is available as an arXiv e-print.