An Operational Semantics for Trust Policies

In the trust-structure model of trust management, principals specify their trusting relationships with other principals in terms of trust policies. In their paper on trust structures, Carbone et al. present a language for trust policies, and provide a suitable denotational semantics. The semantics ensures that for any collection of trust policies, there is always a unique global trust-state, compatible with all the policies, specifying everyone's degree of trust in everyone else. However, as the authors themselves point out, the language lacks an operational model: the global trust-state is a well-defined mathematical object, but it is not clear how principals can actually compute it. This becomes even more apparent when one considers the intended application environment: vast numbers of autonomous principals, distributed and possibly mobile. We provide a compositional operational semantics for a language of trust policies. The operational semantics is given in terms of a composition of I/O automata. We prove that this semantics is faithful to its corresponding denotational semantics, in the sense that any run of the I/O automaton ``converges to'' the denotational semantics of the policies. Furthermore, as I/O automata are a natural model of asynchronous distributed computation, the semantics leads to an algorithm for distributedly computing the trust-state, which is suitable in the application environment

Abstract: