An Abstract Model of a Trusted Platform

A trusted platform is a fundamental building block in most trusted computing based architectures. Although it can be constructed from a finite set of components, there are several ways of combining the components and several configuration options that affect

trust-related

properties. Examples of such properties may be specifying that a platform will not expose a secret or delegate a task to a rogue entity. Despite its importance, very little attention has been directed towards reasoning about the properties that result from the way the platform is constructed and configured. Reasoning about these properties enables one to understand their security implications. In order to reason about such properties, we propose an abstract model, based on CSP, in which a platform is treated as a potentially malicious composition of sub-systems that interact through communication of messages. The model enables instantiation of platforms with varying trust levels and verification against specified properties. The applicability of the model is demonstrated on a trusted grid platform.