© Springer-Verlag Berlin Heidelberg 1997.The aim of access control is to limit what users of distributed systems can do directly or through their programs. As the size of the systems and the sensitivity of data increase formal methods of analysis are often required. This paper presents a prefixed tableaux method for the calculus of access control in distributed system developed at DEC-SRC by Abadi, Lampson et. al. Beside the applicative interest, the calculus poses interesting technical challenges, since it has not the tree-model property, introduces relations between modalities which cannot be compiled into axiom schemas, and has some features of the universal modality. As a side-effect we show a tableaux calculus for the universal modality which distinguishes it from S5 (via satisfiability on non tree-models).
|Name||Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|
|Conference||International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997|
|Period||13/05/97 → 16/05/97|