Affiliations: [a] Computer Science Department, Stanford University, Stanford, CA 94305, USA. E-mail: [email protected], [email protected] | [b] Computer Science Laboratory, SRI International, Menlo Park, CA 94025, USA. E-mail: [email protected]
Note: [*] Supported in part by DARPA contract N66001-00-C-8015 and ONR grant N00014-01-1-0795.
Note: [**] Supported in part by DARPA contract N66001-00-C-8015 and ONR grant N00014-01-1-0837.
Abstract: We present a trust management kernel that clearly separates authorization and structured distributed naming. Given an access request and supporting credentials, the kernel determines whether the request is authorized. We prove soundness and completeness of the authorization system without names and prove that naming is orthogonal to authorization in a precise sense. The orthogonality theorem gives us simple soundness and completeness proofs for the entire kernel. The kernel is formally verified in PVS, allowing for the automatic generation of a verified implementation of a reference monitor. By separating naming and authorization primitives, we arrive at a compositional model and avoid concepts such as “speaks-for” that have led to anomalies in logical characterizations of other trust management systems.
