BRICS RS-03-4 Carbone et al.: A Formal Model for Trust in Dynamic Networks BRICS

Basic Research in Computer Science

A Formal Model for Trust in Dynamic Networks

Marco Carbone Mogens Nielsen Vladimiro Sassone BRICS Report Series RS-03-4 ISSN 0909-0878 January 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Marco Carbone & Mogens Nielsen & Vladimiro

Sassone. BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/03/4/ A Formal Model for Trust in Dynamic Networks

Marco Carbone^{1}, Mogens Nielsen^{1}, Vladimiro Sassone^{2}

1 BRICS^{∗}, University of Aarhus ^{2} COGS, University of Sussex

Abstract. We propose a formal model of trust informed by the Global Computing scenario and focusing on the aspects of trust formation, evolution, and propagation. The model is based on a novel notion of trust structures which, building on concepts from trust management and domain theory, feature at the same time a trust and an information partial order.

Introduction

Global Computing (GC) is an emerging aspect of computer science and technology. A GC system is composed of entities which are autonomous, decentralised, mobile, dynamically configurable, and capable of operating under partial information. Such systems, as e.g. the Internet, become very complex very easily, and have brought forward once again the necessity of guaranteeing security properties. Traditional security mechanisms, however, have severe limitations in this setting, as they are often either too weak to safeguard against the actual risks, or so stringent to impose unacceptable burdens on the effectiveness and flexibility of the infrastructure. Trust management systems, whereby safety critical decision are made based on trust policies and their deployment in the presence of partial knowledge, have an important role to play in GC.

This paper focuses on the foundations of formal models for trust in GC-like environments, capable of underpinning the use of trust-based security mechanisms as an alternative to the traditional ones.

Trust is a fundamental concept in human behaviour, and has enabled collaboration between humans and organisations for millennia. The ultimate aim of our research on trust-based systems is to transfer such forms of collaboration to modern computing scenarios. There will clearly be differences between the informal notion of trust explored in the social sciences and the kind of formality needed for computing. Mainly, our models need in the end to be operational, so as to be implementable as part of GC systems. Equally important is their role in providing a formal understanding of how trust is formed from complex interactions between individuals, so as to support reasoning about properties of trust-based systems.

Although our notion of trusted entity intends to cover only computing entities – even though of variable nature, spanning from soft to hard devices of all sorts – familiarity with trust models from the social sciences is a good starting point for our search

MC and MN supported by ‘SECURE: Secure Environments for Collaboration among Ubiquitous Roaming Entities’, EU FET-GC IST-2001-32486. MC supported by ‘DisCo: Semantic Foundations of Distributed Computation’, EU IHP ‘Marie Curie’ HPMT-CT-2001-00290. VS supported by ‘MyThS: Models and Types for Security in Mobile Distributed Systems’, EU FET-GC IST-2001-32617. ^{∗}Basic Research In Computer Science funded by the Danish National Research Foundation.

of a foundational, comprehensive formal model of trust. One of our main sources has been the work by McKnight and Chervany [16], who provide a typology of trust used to classify existing research on trust in domains like sociology, psychology, management, economics, and political sciences. Trust is thereby classified conceptually in six categories: disposition, when entity a is naturally inclined to trust; situation, when a trusts a particular scenario; structure, when a trusts impersonally the structure b is part of; belief, when a believes b is trustworthy; intention, when a is willing to depend on b; behaviour, when a voluntarily depends on b. Orthogonally, the notion of trustee is classified in categories, the most relevant of which decree that b is trusted because of its competence, benevolence, integrity, or predictability. We believe that a good mathematical model of computational trust should be capable of expressing all such aspects, as well as further notions of primary relevance in computing, e.g. that trust information is time dependent and, in general, varies very rapidly. Also, it should be sufficiently general to allow complex structures representing combinations of different types of trust.

We think of the standard deployment of a trust management system as consisting of a “trust engine” and a “risk engine” coupled together as part of a principal. The trust engine is responsible for updating trust information based on direct and indirect observations or evidence, and to provide trust information to the risk engine as input to its procedures for handling requests. The risk engine will feed back information on principals’ behaviours as updating input to the trust engine. Abstracting over this point of view, we single out as central issues for our trust model the aspects of trust formation, evolution, and propagation. The latter is particularly important in our intended application domain, where the set of active principals is so large and open-ended that centralised trust and ad-hoc methods of propagation of its variations make absolutely no sense. An important propagation mechanism is delegation, whereby principals cooperate to implement complex, intertwined “global” trusting schemes. Just to pin down the idea, bank b may be willing to trust client c to an overdraft limit x only if bank b′trusts it at least up to 2x/3, and c itself does not trust d, a crook known to b. Delegation has important consequences for trust representation, because it brings forward the idea of trust policy, i.e. algorithmic rules – such as bank b’s above – to evaluate trust requests. In principle, trust among principals can be represented straightforwardly, as a function from pairs of principals to trust levels,

GlobalTrust : Principal −→ Principal −→ TrustDegree

where GlobalTrust (a) is a function which associates to each principal b the value of a’s trust in b. Delegation leads to model local policies, say b’s, as functions

TrustPolicy : GlobalTrust −→ Principal −→ TrustDegree

where the first argument is (a representation of) a universal trust function that b needs to know b′’s level of trust in c and whether or not c trusts d.

The domain of TrustPolicy makes the core of the issue clear: we are now entangled in a “web of trust,” whereby each local policy makes references to other principals’ local policies. Technically, this means that policies are defined by mutual recursion, and global trust is the function determined collectively by the web of policies, the function that stitches them all together. This amounts to say that GlobalTrust is the least fixpoint of the universal set of local policies, a fact first noticed in [21] which leads straight to domain theory [20]. Domains are kinds of partially ordered sets which underpin the semantic theory of programming languages and have therefore been studied extensively. Working with domains allows us to use a rich and well-established theory of fixpoints to develop a theory of security policies, as well as flexible constructions to build structured trust domains out of basic ones. This is precisely context and the specific contribution of this paper, which introduces a novel domain-like structure, the trust structures, to assign meaning and compute trust functions in a GC scenario. We anticipate that, in due time, techniques based on such theories will find their way as part of trust engines.

As domains are partial orders (actually CPOs) and trust degrees naturally come equipped with an ordering relation (actually a lattice structure), a possible way forward is to apply the fixpoint theory to TrustDegree viewed as a domain. This is indeed the way of [21] and, as we motivate below, it is not a viable route for GC. There are about a million reasons in a dynamic “web of trust” why a principal a trying to delegate to b about c may not get the information it needs: b may be temporarily offline, or in the process of updating its policy, or experiencing a network delay, or perhaps unwilling to talk to a. Unfortunately, the fixpoint approach would in such cases evaluate the degree of trust of a in c to be the lowest trust level, and this decision would be wrong. It would yield the wrong semantics. Principal a should not distrust c, but accept that it has not yet had enough information to make a decision about c. What is worst with this way of confusing “trust” with “knowledge,” is that the information from b could then become available a few millisecond after a’s possibly wrong decision.

We counter this problem by maintaining two distinct order structures on trust values: a trust ordering and an information ordering. The former represents the degree of trustworthiness, with a least element representing, say, absolute distrust, and a greatest element representing absolute trust; the latter the degree of precision of trust information, with a least element representing no knowledge and a greatest element representing certainty. The domain-theoretic order used to compute the global trust function is the information order. Its key conceptual contribution is to introduce a notion of “uncertainty” in the trust value principals obtain by evaluating their policies. Its technical contribution is to provide for the “semantically right” fixpoint to be computed.

Following this lead, we introduce and study trust structures of the kind (D,⪯,⊑), where the two order relations carry the meaning illustrated above; we then provide constructions on trust structures – including an “interval” construction which introduce a natural notion of uncertainty to complete lattices to lift them to trust structures – and use the results to interpret an toy, yet significant policy language. We believe that introducing the information ordering alongside the trust ordering is a significant step towards a model of trust feasible in a GC scenario; it is a major point of departure from the work of Weeks [21], and the central contribution of this paper.

Plan of the document. In §1 we define our trust model along the lines illustrated above, whilst §2 focuses on trust structures, providing methods for constructing useful structures as well as a general method to add uncertainty to the model. In §3 we introduce a policy language and use our trust structure to give it a denotational semantics.

Related Work. Trust is a pervasive notion and, as such, has been studied thoroughly in a variety of different fields, including social sciences, economics and philosophy. Here we only survey recent results on trust as a subject in computing. The reader is referred to [16] for a broader interpretation. A detailed survey can be found in Grandison and Sloman’s [10].

Most of the existing relevant work concerns system building. In [19], Rivest et al. describe SDSI, a public key infrastructure featuring a decentralised name space which allows principals to create their own local names to refer to other principals’ keys and in general, names. Ellison et al. [9] proposed a variation of the model which contributes flexible means to specify authorisation policies. The proposals are now merged in a single approach, dubbed SPKI/SDSI. Other systems of practical relevance include PGP [24], based on keys signed by trusted certificating authorities; KeyNote [3], which provides a single, unified language for both local policies and credential containing predicates to describe the trusted actions granted by (the holders of) specific public keys; PolicyMaker [2], an early version of KeyNote; and REFEREE [6], which uses a tri-valued logic which enriches the booleans with a value unknown. Trust in the framework of mobile agents is discussed e.g. in [22]. Delegation plays a relevant rôle in trustbased distributed systems. A classification of delegation schemes is proposed by Ding et al. [8], where they discuss implementation and analyse appropriate protocols. The ideas expressed in [8] lie at a different level from ours, as the focus there is exclusively on access control.

The theoretical work can be broadly divided in two main streams: logics, where the trust engine is responsible for constructing [5, 4, 12–14] or checking [1] a proof that the desired request is valid; and computational models [21, 7], like our approach.

Burrows et al. propose the BAN logic [5], a language for expressing properties of and reasoning about the authentication process between two entities. The language is founded on cryptographic reasoning with logical operators dealing with notions of shared keys, public keys, encrypted statements, secrets, nonce freshness and statement jurisdiction. In [4], Abadi et al. enhance the language by introducing delegation and groups of principals: each principal can have a particular role in particular actions. The Authorisation Specification Language (ASL) by Jajodia et al. [12] separates explicitly policies and basic mechanisms, so as to allow a more flexible approach to the specification and implementation of trust systems. ASL supports under a common architectural framework both the closed policy model, whereby all allowable accesses must be specified, and the open policy model, where are the denied accesses which must be explicitly specified. It also supports role-based access control.

Modal logics have a relevant place in specifying trust models, and have been used to express possibility, necessity, belief, knowledge, temporal progression, and more. Jones and Firozabadi [13] address the issue of the reliability of an agent’s transmission using a modal logic of actions [17] to model agents. Rangan [18] views a distributed system as a collection of communicating agents in which an agent’s state is the history of its messages, and formalises the accessibility relation which describes systems’ dynamics. Rangan’s model builds on simple trust statements used to defined simple properties, such as transitivity and the Euclidean property, which are then used to specify systems and analyse them with respect to properties of interest. Recently, Jøsang [14] proposed a logic of uncertain probabilities, a work which is related to our interval construction and can be recast as an instance of it in our framework. Specifically, Jøsang considers intervals of belief and disbelief over real numbers between 0 and 1.

Concerning computational models, Weeks [21] provides a model based on fixpoint computations which is of great relevance to our work. Winsborough and Li [23] study automated trust negotiation, an approach to regulate the exchange of sensitive credentials in untrusted environments. Clarke et al. [7] provide an algorithm for “certificate chain discovery” in SPKI/SDSI whereby principal build coherent chains of certificates to request and grant trust-based access to resources.

1 A Model for Trust

The introduction has singled out the traits of trust most relevant to our computational scenario: trust involves entities, has a degree, is based on observations and ultimately determines the interaction among entities. Our model will target these aspects primarily.

Entities will be referred to as principals. They form a set P ranged over by a,b,c,... and p. We assume a set T of trust values whose elements represent degrees of trust. These can be simple values, such as {trusted, distrusted}, or also structured values, e.g. pairs where the first element represents an action, say access a file, and the second a trust level associated to that action; or perhaps vectors whose elements representing benevolence in different situations.

As trust varies with experience, a model should be capable of dealing with observations resulting from the principal’s interaction with the environment. For clarity, let us isolate the principal’s trust management from the rest of its behaviour, and think of each principal as having a “module” containing all its trust management operations and data. Thinking “object-oriented,” we can envision this as an object used by the principal for processing trust related information. Assuming a set of observations O relevant to the concrete scenario of interest, the situation could be depicted as below.

request [figure] - updateTrust : O −→ void - trustValue : P −→ T [figure] t ∈ T

The principal sends the message trustValue (p) to ascertain its trust in another principal p, and the message updateTrust(o) to add the observation o to its trust state.

In this paper, we only focus on the trust box and assume, without loss of generality, that the remaining parts of the principal interact with it using the two methods illustrated above, or some similarly suitable interface.

Modelling the Trust Box

Principals’ trust in each other can be modelled as a function which associates to each pair of principals a trust value in t ∈ T :

m: P −→ P −→ T

Function m applied to a and then to b returns the trust value m(a)(b) ∈ T expressing a’s trust in b. This however does not mean that a single principal’s trust can be modelled as a function from P to T , since a’s trust values may depend on other principals’ values. For instance, a may wish to enforce that its trust in c is b’s trust in c. Similarly, we may be willing to receive a message from unknown sources, provided somebody we know trusts the sender. This mechanism of relying on third-party assessments, called delegation, is fundamental in all scenarios involving cooperation, including computational paradigms such as Global Computing.

This leads us to a refined view of a principal’s trust as being defined by a policy. According to such view, each principal has a local policy π which contributes by way of delegation to form the global trust m. A policy expresses how the principal computes trust information given not just his own beliefs, but also other principals’ beliefs. It follows that a’s policy π_{a} has the type below, whose first argument represents the knowledge of third principals’ policies that a needs to evaluate π_{a}.

π_{a} : (P −→ P −→ T ) −→ (P −→ T )

In this paper we leave unspecified the way a policy is actually defined, as this definitely depends on the application. We study a relevant example of policy language in §3.

By collecting together the individual policies, we obtain a function Π ≜ λp: P .π_{p} whose type is (isomorphic to)

Π: (P −→ P −→ T ) −→ (P −→ P −→ T ).

To interpret this collection of mutually recursive local policies as a global trust function m, we apply some basic domain theory, namely fixpoints and complete partial orders. We recall below the main notions involved; in general we assume the reader to be acquainted with partial orders (cf. [11] for a thorough introduction). Given a partial order (T,⊑), an ω-chain c is a monotone function from the set of natural numbers ω to T; that is c = (c_{n})_{n∈ω} such that c_{0} ⊑ c_{1} ⊑ c_{2} ⊑ ...

Definition 1 (CPOs and Continous functions). A partial order (T,⊑) is a complete partial order (CPO) if it has a least element ⊥ and each ω-chain c in T has a least upper bound ⨆ c. A function f between CPOs is continuous if for each ω-chain c, it holds that ⨆ f(c) = f(⨆ c).

The importance of CPOs here is that every continuous function f : (T,⊑) → (T,⊑) on a CPO has a least fixpoint fix(f) ∈ T, that is the least x such that f(x) = x (cf. [20]). So, requiring T to be a CPO, which implies that P → P → T is a CPO too, and taking Π to be continuous, let us define global trust as m ≜ fix(Π), the least fixpoint of Π.

The question arises however as to what order to take for ⊑. We maintain that it cannot be the order which measures the degree of trust. An example is worth many words. Let T be the CPO {low ≤ medium≤ high}, and consider a policy π_{a} which delegates to b the degree of trust to assign to c. In this setup, a will assign low trust to c when it is not able to gather information about c from b. This however would clearly be an erroneous conclusion, as the interruption in the flow of information does not bear any final meaning about trust, its most likely cause being a transient network delay that will soon be resolved. The right conclusion for a to draw is not to distrust c, but to acknowledge that it does not know (yet) whether or not to trust c. In other words, if we want to model dynamic networks, we cannot allow confusion between “don’t trust” and “I don’t know:” the latter only means lack of evidence for trust or distrust, the former implies a trust-based, possibly irreversible decision.

Thus, in order to make sense of our framework, we need to introduce a notion of uncertainty of trust values. Truthful to the Global Computing scenario, we so account for the fact that principals may have only a partial knowledge of their surroundings and, therefore, of their own trust policies. We address this by considering approximate trust values which embody a level of uncertainty as to which value we are actually presented with. Specifically, beside the usual trust value ordering, we equip trust values with a trust information ordering. While the former measures the degree of trustworthiness, the latter measures the degree of uncertainty present in our trust information, that is its information content. We will assume that the set T of (approximations of) trust values is a CPO with an ordering relation ⊑. Then t ⊑ t′means that t′“refines” t, by providing more information than t about what trust value it approximates. With this understanding the continuity of Π is a very intuitive assumption: it asserts that the better determined the information from the other principals, the better determined is value returned by the policy. An example will help to fix these ideas.

Example 1. Let us refine the set of trust values T seen above by adding some intermediate values, viz. T = {⊥,∗,low,medium,high}, and consider the information ordering ⊑ specified by the following Hasse diagram:

[figure: high; medium; *; low; ⊥]

This ordering says nothing about comparing degrees of trust. It focuses only on the quantity of information contained in values. The element ∗ represents the uncertainty as to whether high or medium holds, while ⊥ gives no hint at all about the actual trust value. The limit of a chain reflects the finest information present in it, as a whole. Suppose we have a set of principal P = {a,b,c} with the following policies:

a  b  c
a high  ⊥  ask b
b  ∗  high  low
c ask b  high  high

where each row is a principal’s policy. For instance the third row gives c’s policy: c’s trust in a is b’s trust in a; c’s trust in b is high. The computation of the least fixpoint happens by computing successive approximations following the standard theory, as illustrated below. We start from the least possible trust function:

a  b  c
a  ⊥  ⊥  ⊥
b  ⊥  ⊥  ⊥
c  ⊥  ⊥  ⊥

where there is absolute no knowledge and so any trust value could be anything, hence ⊥. Each principal then inspects its own policy, and computes an approximated value using the other principals’ current approximations of their values.

a  b  c
a high  ⊥  ⊥
b  ∗  high  low
c  ⊥  high  high

Observe that here a is still totally undecided as to the trust to assign to c, as it knows that the value ⊥ received from b is itself uncertain. The successive iteration is however enough to solve all solvable uncertainties, and reach the global trust function (that is the last fixpoint) illustrated below.

a  b  c
a high  ⊥  low
b  ∗  high  low
c  ∗  high  high

We reiterate that, importantly, the ordering ⊑ is not to be identified with the equally essential ordering “more trust.”

Example 2 (Collecting Observations). In order to exemplify the idea of a trust structure with two distinct orders, assume that each observation can be classified either to be positive or negative. Then let T be the set of pairs {(p,n)|p,n ∈ ω + {∞}, p ≤ n} where p stands for the number of positive experience and n for the total number of experiences. A suitable information ordering here would be

(p_{1},n_{1}) ⊑ (p_{2},n_{2}) iff n_{1} ≤ n_{2},

with (0,0) being the least element. This formalises the idea that the more experience we make, the more knowledge we have. That is, trust information becomes more and more precise with interactions. On the other hand, it is intuitively clear that negative experiences cannot lead to higher trust. Therefore, a suitable trust ordering could be

(p_{1},n_{1}) ⪯ (p_{2},n_{2}) iff p_{1} ≤ p_{2}.

2 Trust Structures

Having pointed out the need for order structures equipped at the same time with an information and a trust ordering, in this section we focus on the triples (T ,⪯,⊑), which we call trust structures, and study their basic properties. The notion of complete lattice, recalled below, will play a relevant role.

Definition 2 (Complete lattice). A partial order (D,≤) is a complete lattice if every X ⊆ D has a least upper bound (lub) and, as a consequence, a greatest lower bound (glb). We use ∨ and ∧ to denote, respectively, lubs and glbs in lattices.

When defining a trust management system, it is natural to start off with a set D of trust values, or degrees. On top of that, we are likely to need ways to compare and combine elements of D so as to form, say, a degree which comprehends a given set of trust values, or represents the trust level common to several principals. This amounts to start with a complete lattice (D,≤), where those combinators can be considered as taking lub’s or glb’s of sets of values. But, as illustrated above, this is not yet enough for understanding a trust framework as we need to account for uncertainty. To this purpose we define an operator I to extend a lattice (D,≤) to a trust structure (T ,⪯,⊑). The set T consists of the set of intervals over D which, besides containing a precise image of D – viz. the singletons – represent naturally the notion of approximation, or uncertainty about elements of D.

Interval Construction

We define now the ordering ⪯ which has been already considered in [15].

Definition 3. Given a complete lattice (D,≤) and nonempty subsets X,Y ⊆ D we say that X ⪯ Y if and only if

∧X ≤ ∧Y  and  ∨ X ≤ ∨Y

Clearly, ⪯ is not a partial order on the subsets of D, as the antisymmetry law fails. We get a partial order by considering as usual the equivalence classes of ∼ = ⪯ ∩ ⪰ . It turns out that the intervals over D are a set of representatives of such classes.

Definition 4. For (D,≤) a complete lattice, I(D) = {[d_{0},d_{1}] | d_{0},d_{1} ∈ D, d_{0} ≤ d_{1}}, where [d_{0},d_{1}] = {d |d_{0} ≤ d ≤ d_{1}} is the interval of D determined by d_{0} and d_{1}.

Proposition 1. Let X = [d_{0},d_{1}] be an interval in D. Then, ∧X is d_{0} and ∨X is d_{1}.

As a consequence of the proposition above we have that X ∼ [∧X,∨X], for all X ⊆ D. Furthermore, [d_{0},d_{1}] ∼ [d′_{0},d′_{1}] implies that d_{0} = d′_{0} and d_{1} = d′_{1}.

The following lemma characterises ⪯ in terms of ≤.

Lemma 1. For [d_{0},d_{1}] and [d′_{0},d′_{1}] intervals of D, we have [d_{0},d_{1}] ⪯ [d′_{0},d′_{1}] if and only if d_{0} ≤ d′_{0} and d_{1} ≤ d′_{1}.

We can now show that the lattice structure on (D,≤) is lifted to a lattice structure (I(D),⪯) on intervals.

Theorem 1. (I(D),⪯) is a complete lattice.

Proof. Let S be a subset of I(D). We prove that its least upper bound exists. Observe that this is enough to conclude, as ⋀ X is equal to ⋁ {y|y ⪯ x for all x ∈ X }. Let S be {[d_{0}^{i},d_{1}^{i}]|i ∈ J} for some set J. We claim that ⋁ S = [∨d_{0}^{i},∨d_{1}^{i}].

As d_{0}^{i} and d_{1}^{i} are elements of a complete lattice ∨d_{0}^{i} and ∨d_{1}^{i} exist. Moreover for each j we have d_{0}^{j} ≤ d_{1}^{j} ≤ ∨d_{1}^{i}, so ∨d_{0}^{i} ≤ ∨d_{1}^{i} which implies [∨d_{0}^{i},∨d_{1}^{i}] ∈ I(D). Also, [∨d_{0}^{i},∨d_{1}^{i}] is an upper bound as for each j we have [d_{0}^{j},d_{1}^{j}] ⪯ [∨d_{0}^{i},∨d_{1}^{i}]. Finally, [∨d_{0}^{i},∨d_{1}^{i}] is the least upper bound: if for each j we have that [d_{0}^{j},d_{1}^{j}] ⪯ [d_{0},d_{1}] then [∨d_{0}^{i},∨d_{1}^{i}] ⪯ [d_{0},d_{1}]. This holds since d_{0}^{j} ≤ d_{0} and d_{1}^{j} ≤ d_{1} which means that ∨d_{0}^{i} ≤ d_{0} and ∨d_{1}^{i} ≤ d_{1}. □

We define an ordering on intervals which reflects their information contents so to complete the lattice structure with a CPO to base fixpoint computations on. The task is quite easy: as the interval [d_{0},d_{1}] expresses a value between d_{0} and d_{1}, the narrower the interval, the fewer the possible values. This leads directly to the following definition.

Definition 5. For (D,≤) a complete lattice and X,Y ∈ I(D), define X ⊑ Y if Y ⊆ X.

Analogously to ⪯, we can characterise ⊑ in terms of ≤. The proof follows a similar patter and is therefore omitted.

Lemma 2. For [d_{0},d_{1}] and [d′_{0},d′_{1}] intervals of D, we have that [d_{0},d_{1}] ⊑ [d′_{0},d′_{1}] if and only if d_{0} ≤ d′_{0} and d′_{1} ≤ d_{1}.

Finally, as for the previous ordering, we have the following result.

Theorem 2. (I(D),⊑) is a CPO.

Proof. The least element of (I(D),⊑) is D = [∧D,∨D]. Let [d_{0}^{n},d_{1}^{n}]_{n} be an ω-chain in (I(D),⊑). Then we claim that ⨆ [d_{0}^{n},d_{1}^{n}]_{n} = [∨d_{0}^{n},∧d_{1}^{n}]. We need to prove that this is well-defined and that it is the least upper bound.

As in the proof of Theorem 1, ∨d_{0}^{i} and ∧d_{1}^{i} exist. Moreover, if for all i and j it holds that d_{0}^{i} ≤ d_{1}^{j}, then for all j we have that ∨d_{0}^{i} ≤ d_{1}^{j}, hence ∨d_{0}^{i} ≤ ∧d_{1}^{i}, which implies that [∨d_{0}^{n},∧d_{1}^{n}] is well defined. Interval [∨d_{0}^{n},∧d_{1}^{n}] is an upper bound as for all j it holds that [d_{0}^{j},d_{1}^{j}] ⊑ [∨d_{0}^{i},∧d_{1}^{i}]. In fact for all j we have d_{0}^{j} ≤ ∨d_{0}^{i} and ∧d_{1}^{i} ≤ d_{1}^{j}, which means [∨d_{0}^{i},∧d_{1}^{i}] ⊑ [d_{0}^{j},d_{1}^{j}]. Finally, [∨d_{0}^{n},∧d_{1}^{n}] is the least upper bound as for any interval [d_{0},d_{1}] if [d_{0}^{j},d_{1}^{j}] ⊑ [d_{0},d_{1}] for all j then [∨d_{0}^{i},∧d_{1}^{i}] ⊑ [d_{0},d_{1}]. In fact d_{0}^{j} ≤ d_{0} and d_{1} ≤ d_{1}^{j}. By definition of lub and glb we have that ∨d_{0}^{i} ≤ d_{0} and d_{1} ≤ ∧d_{1}^{i}. □

The trust structures above give a constructive method to model trust based systems. We remark that intervals are a natural way to express partial information: trust in a principal is [d_{0},d_{1}] when it could be any value in between d_{0} and d_{1}.

Example 3 (Intervals in [0,1]). Let R stand for the set of reals between 0 and 1, which is a complete lattice with the usual ordering ≤. We can now consider the set I(R) of intervals in R. From the previous results it follows that (I(R),⪯) is a complete lattice and (I(R),⊑) is a complete partial order. Hence, if we start with a domain of trust values which are elements in R we can apply our model to the new domains. This kind of construction on reals is related to the uncertainty logic [14] where an interval [d_{0},d_{1}] in I(R) is seen as a pair of numbers where d_{0} is called belief and 1 − d_{1} disbelief. This new trust domain is particularly interesting since it allows to express complex policies. We shall see a few examples later on.

Lifting Operators

The continuity of the function Π is an important requirement. This property depends on the operators used with the policies. In the sequel we give a useful result, wrt our interval construction, which allows to lift continuous operators in the original lattice (D,≤) to continuous operators in (I(D),⊑) and (I(D),⪯).

Definition 6. For (D,≤) and (D′,≤′) complete lattices and f : D −→ D′a continuous function, let I(f) : I(D) −→ I(D′) be the pointwise lifting of f defined as

I(f)([d_{0},d_{1}]) = [f(d_{0}),f(d_{1})].

In the definition above, note that the continuity of f ensures that I(f) is well defined. An ω-cochain in a complete lattice (D,≤), is an antitone function c : ω → T, that

is a function such that i ≤ j implies c_{j} ≤ c_{i}. A function f : (D,≤) −→ (D′,≤′) is co-continuous iff for each ω-cochain c in D, it holds that ⋀ f(c) = f(⋀ c); f is bicontinuous if it is continuous and co-continuous.

The following proposition states that ω-cochains in (I(D),⊑) have glbs.

Proposition 2. Let [d_{0}^{n},d_{1}^{n}] be an ω-cochain in (I(D),⊑). Then [d_{0}^{n},d_{1}^{n}] = [∧d_{0}^{n},∨d_{1}^{n}].

Proof. The proof proceeds symmetric to that of Theorem 2. □

We can now give the following result about lifted functions in trust structures.

Theorem 3. For (D,≤) and (D′,≤′) complete lattices and f : D −→ D′a bi-continuous function, the pointwise lifting I(f) is bi-continuous with respect both the information and the trust orderings.

Proof. We show that I(f) is bi-continuous with respect to the information ordering. First we prove that I(f) is continuous, i.e. ⨆ I(f)([d_{0}^{n},d_{1}^{n}]) = I(f)(⨆ [d_{0}^{n},d_{1}^{n}]) for [d_{0}^{n},d_{1}^{n}] an ω-chain. By definition of I(f) we have that ⨆ I(f)([d_{0}^{n},d_{1}^{n}]) = ⨆ [f(d_{0}^{n}),f(d_{1}^{n})] and from the proof of Theorem 2 and bi-continuity of f it follows that

⨆ [f(d_{0}^{n}),f(d_{1}^{n})] = [∨f(d_{0}^{n}),∧f(d_{1}^{n})] = [f(∨d_{0}^{n}),f(∧d_{1}^{n})] = I(f)(⨆ [d_{0}^{n},d_{1}^{n}]).

The proof that I(f) is co-continuous follows the same patterns. Let [d_{0}^{n},d_{1}^{n}] be an ωcochain. Then, I(f)([d_{0}^{n},d_{1}^{n}]) = [f(d_{0}^{n}),f(d_{1}^{n})] and from the proposition above and by the bi-continuity of f it follows that

[f(d_{0}^{n}),f(d_{1}^{n})] = [∧f(d_{0}^{n}),∨f(d_{1}^{n})] = [f(∧d_{0}^{n}),f(∨d_{1}^{n})] = I(f)( [d_{0}^{n},d_{1}^{n}]).

The proof for the trust orderings proceeds similarly. □ In the following examples we show how to apply the previous theorem to some

interesting operators.

Example 4 (Lub and glb operators). The most natural operators, regarding lattices, are lub and glb. It is easy to see that they are bi-continuous in (D,≤) complete lattice. Exploiting Theorem 3 we can now state that lub and glb wrt ⪯ are bi-continuous over (I(D),⊑).

Example 5 (Multiplication and Sum). When considering the interval construction over R, as in Example 3, we can lift the operators of sum (weighed) and multiplication over the intervals. In fact, given two intervals [d_{0},d_{1}] and [d′_{0},d′_{1}], the product is defined as

[d_{0},d_{1}] · [d′_{0},d′_{1}] = [d_{0}· d′_{0},d_{1}· d′_{1}].

which is exactly the lifting of multiplication over reals. Similarly we can define sum as

[d_{0},d_{1}] + [d′_{0},d′_{1}] = [d_{0}+ d′_{0}− d_{0}· d′_{0},d_{1}+ d′_{1}− d_{1}· d′_{1}]

These operations appears in [14] under the names of conjunction and disjunction.

Example 6 (A non-lifted operator: Discounting). Discounting, as defined in [14], is an operator which weighs the trust value received from a delegation according to the trust in the delegated principal.

[d_{0},d_{1}] ▷ [d′_{0},d′_{1}] = [d_{0}· d′_{0},1 − d_{0}· (1 − d′_{1})]

Notice that this operator is not commutative.

2.1 Product and Function Constructors

Our model should satisfy “context dependent” trust. By this we mean that trusting a principal a to obtain information about restaurants does not mean that we trust a about, say, sailing. We can accommodate this kind of situations using a simple property of lattices and CPO’s. Namely, we can form products of trust structures where each component accounts for a particular context. For instance, using a domain of the form Restaurants × Sailing will allow us to distinguish about a’s dependability on the two issues of our example. The next theorem shows that extending the orders pointwise to products and function spaces gives the result we need.

Theorem 4. Given two complete lattices (D,≤), (D′,≤′) and a generic set X then

1. I(D × D′) is isomorphic to I(D) × I(D′);

2. X −→ I(D) is isomorphic to I(X −→ D).

Proof. In both cases we have to show that there exists a bijective correspondence H which preserves the orderings. We use as usual (d,d) to denote pairs and λx.t(x) to express the function which takes a value d and returns t(d).

1. Let [(d_{0},d′_{0}),(d_{1},d′_{1})] and [(d_{2},d′_{2}),(d_{3},d′_{3})] be in I(D×D′). We define the function H : I(D × D′) −→ I(D) × I(D′) by

H([(d_{0},d′_{0}),(d_{1},d′_{1})]) = ([d_{0},d_{1}],[d′_{0},d′_{1}])

which is easily seen to be bijective. We first show that H is well defined, i.e. that d_{0} ≤ d_{1} and d′_{0} ≤′d′_{1}. This follows at once, since (d_{0},d′_{0}) ≤_{D×D′} (d_{1},d′_{1}) where ≤_{D×D′} is the pointwise extension of ≤ and ≤′. Next we prove that H preserves and reflects ⪯. This amounts to prove that

[(d_{0},d′_{0}),(d_{1},d′_{1})]⪯_{I(D×D′)} [(d_{2},d′_{2}),(d_{3},d′_{3})]  (1)

if and only if

([d_{0},d_{1}],[d′_{0},d′_{1}])⪯_{I(D)×I(D′)} ([d_{2},d_{3}],[d′_{2},d′_{3}])  (2)

By Lemma 1, relation (1) above holds if and only if

(d_{0},d′_{0}) ≤_{D×D′} (d_{2},d′_{2}) and (d_{1},d′_{1}) ≤_{D×D′} (d_{3},d′_{3}).  (3)

Then, by the same Lemma 1, property (3) holds if and only if

[d_{0},d_{1}] ⪯_{I(D)} [d_{2},d_{3}] and [d′_{0},d′_{1}] ⪯_{I(D′)} [d′_{2},d′_{3}],

which is the same as saying that (2) holds. The proof is similar for the information ordering.

2. Let [f_{0},f_{1}] and [f′_{0},f′_{1}] be in I(X −→ D) and g in X −→ I(D). We define the bijection H : I(X −→ D) ≅ (X −→ I(D)) by H([f_{0},f_{1}]) = λx.[f_{0}(x),f_{1}(x)]. It is easy to see that H([f_{0},f_{1}]) is well defined. The function H^{−1} (g) = [λx. ∧ g(x),λx. ∨ g(x)] is the inverse of H. In fact, H^{−1} (H([f_{0},f_{1}])) = H^{−1} (λx.[f_{0}(x),f_{1}(x)]) and by definition of H^{−1} we have that the latter coincides with

[λy. ∧ (λx.[f_{0}(x),f_{1}(x)])(y),λy. ∨ (λx.[f_{0}(x),f_{1}(x)])(y)],

which is [λx. ∧ [f_{0}(x),f_{1}(x)],λx. ∨ [f_{0}(x),f_{1}(x)]], i.e. [f_{0},f_{1}]. Conversely, we have H(H^{−1} (g)) = H([λx.∧g(x),λx.∨g(x)]) and, by definition of H, this is the same as

λy.[(λx. ∧ g(x))(y),(λx. ∨ g(x))(y)] = λx.[∧g(x),∨g(x)] = g.

We now need to show that H and H^{−1} preserve ⊑. Regarding H we have to prove

[f_{0},f_{1}] ⊑_{I(X−→D)} [f′_{0},f′_{1}]  (4)

implies

λx.[f_{0}(x),f_{1}(x)]⊑_{X−→I(D)} λx.[f′_{0}(x),f′_{1}(x)]  (5)

From Lemma 2 and (4) it follows that f_{0} ⊑_{X−→D} f′_{0} and f′_{1}⊑_{X−→D} f_{1} and, as the ordering is pointwise, we have that for all x, f_{0}(x) ≤ f′_{0}(x) and f′_{1}(x) ≤ f_{1}(x). Again by Lemma 2, we obtain [f_{0}(x),f_{1}(x)] ⊑ [f′_{0}(x),f′_{1}(x)] which, by pointwise ordering, implies (5). Regarding H^{−1} , we show that

g ⊑_{X−→I(D)} g′  (6)

implies

[λx. ∧ g(x),λx. ∨ g(x)]⊑_{I(X−→D)} [λx. ∧ g′(x),λx. ∨ g′(x)]  (7)

From (6) we have that, for any x, [∧g(x),∨g(x)] ⊑ [∧g′(x),∨g′(x)]. It then follows that ∧g(x) ≤ ∧g′(x) and ∨g′(x) ≤ ∨g(x) which implies λx.∧g(x) ≤ λx.∧g′(x) and λx. ∨ g′(x) ≤ λx. ∨ g(x). Finally, again by Lemma 2, we have that (7) holds. The proof for the trust ordering is similar and, thus, omitted. □

Remark 1. Theorem 3 holds for any bi-continuous function f : D_{0} × ...× D_{n} −→ D. The pointwise lifting of f gives I(f) : I(D_{0} × ...× D_{n}) −→ I(D) and from the result above we have that I(f) is (isomorphic to) a function F : I(D_{0}) × ...× I(D_{n}) −→ I(D).

3 A Policy Language

Following our discussion we propose to operate with a language for trust policies capable of expressing intervals, delegation, and a set of function constructions. We exemplify the approach by studying the simple policy language below

Syntax

The language consists of the following syntactic categories, parametric over a fixed trust lattice (D,≤).

π::= ⌜p⌝  (delegation) p::= a ∈ P  (principal)
| λx: P . τ  (abstraction)  | x: P  (vars)
τ::= [d,d] ∈ I(D) (value/var) e::= ι eq ι  ι ∈ {τ,p}  (equality)
| π(p)  (policy value)  | τ cmpτ  (comparison)
| e ↦ τ;τ  (choice)  | e bope  (boolean op)
| op(τ_{1}...τ_{n})  (lattice op)

Here op is a continuous function over (I(D),⊑); operator eq is equality in τ ∪ p, cmp is one of ⊑ and ⪯, and bop is a standard boolean operator. The elements of the category p are either principals or variables.

The main syntactic category is π: it can be either delegation to another principal or a λ-abstraction. An element of τ can be an interval, the application of a policy, a conditional or the application of a continuous operator op. The elements of e are boolean functions applied to elements of P, D and I(D).

Semantics

We provide a formal semantics for the language described above. As pointed out before, π is a policy. Hence the semantic domain, as described in §1, will be the codomain of the function

[[π]]_{σ} : (P −→ P −→ T ) −→ (P −→ T ),

where σ is an assignment of values in P to variables. The semantic function [[·]]_{σ} is defined by structural induction on the syntax of π as follows.

[[⌜p⌝]]_{σm}= m([p])_{σm};
[[λx: P. τ]]_{σm}= λp: P .([τ])_{σ{p/x}m}.

Here ([·])_{σm} is a(n overloaded) function which given an assignment σ and a global trust function m: P −→ P −→ T maps elements of p, τ, and e respectively to the semantic domains P, I(D), and Bool as follows.

([ [d_{0},d_{1}] ])_{σm}= [([d_{0}])_{σm},([d_{1}])_{σm}]
([π(p)])_{σm}= [[π]]_{σm}([[p]]_{σm})
([e ↦ τ_{1};τ_{2}])_{σm}= if ([e])_{σm} then ([τ_{1}])_{σm} else ([τ_{2}])_{σm}
([op(τ_{1}...τ_{n})])_{σm}= op(([τ_{1}])_{σm},...,([τ_{n}])_{σm})
([a])_{σm}= a
([x])_{σm}= σ(x)

We omit the rules for the syntactic category e, as they are obvious.

Let {π_{p}}_{p∈P} be a an arbitrary collection of all policies, where π_{p} = λx: P . ⊥ for all but a finite number of principals. The fixpoint semantics of {π_{p}}_{p∈P} is the global trust function determined by the collection of individual policies, and it is readily expressed in terms of [[·]]_{σ}:

{[ {π_{p}}_{p∈P} ]}_{σ} = fix(λm.λp.[[π_{p}]]_{σm})

We believe that this policy language is sufficiently expressive for most application scenarios in global computing, as illustrated by our examples which follows. Note however that our approach easily generalises to any choice of underlying trust structure (T ,⪯,⊑). The only requirement is that the operators used in the policy language are continuous with respect to the information ordering

Example 7 (Read and Write access). Let D = {N,W ,R,RW } represent the access rights to principal’s CVs. The set D is ordered by the relation ≤

∀d ∈ D.N≤ d and ∀d ∈ D.d ≤ RW

We now show how to express some simple of policies in our language. For instance the following policy says that LIZ’s trust in BOB is at least [W,RW] and depends on what she thinks of CARL. Instead, LIZ’s trust in CARL will depend on her trust in BOB: if it is above [W,W] then [R,RW] otherwise [N,RW].

π_{LIZ} = λx: P . x = BOB↦ [W,RW] ∨ ⌜LIZ⌝(CARL );

x = CARL ↦ ([W,W]⪯ ⌜LIZ⌝(BOB ) ↦ [R,RW];[N,RW] ); [N,RW]

We could also extend the previous policy making it dependent on someone else’s belief. For instance, in the following policy, the previous judgement wrt BOB has been merged with PAUL’s belief (weighed by discounting).

π_{LIZ} = λx: P . x = BOB↦ [N,W]∨ ⌜LIZ⌝(CARL ) ∨ ⌜LIZ⌝(PAUL ) ▷ ⌜PAUL ⌝(x);

x = CARL ↦ ([W,W]⪯ ⌜LIZ⌝(BOB ) ↦ [R,RW];[N,RW] ); [N,RW]

In this case LIZ’s trust in PAUL is the bottom value [N,RW] which is going to be the left argument of the discounting operator ▷.

Example 8 (Spam Filter). Let R be the subset of real numbers between 0 and 1 ordered by the usual ≤, as in Example 3. We can now show some policies modelling spam filters for blocking certain emails considered spam. The set of principals P is the set of internet domains from which we could receive emails, e.g. daimi.au.dk. A starting policy, where we suppose that our server spam.filter.edu knows no one, could be the following

π_{1} = λx: P . x = spam.filter.edu ↦ [1,1];[0,1],

meaning that only internal emails are trusted. It could happen that spam.filter.edu starts interacting with other principals. A likely event is that it receives a list of other university internet domains, and decides to almost fully trust them and actually use their beliefs. Then we would have

π_{2} = λx: P . x ∈ UniList ↦ [.75,1]; ⋁_{y∈Unilist}⌜y⌝(x) ∨ π_{1}(x),

where we suppose that “∈” stands for a chain of nested conditionals for all the elements of UniList. Let us suppose now that the filter receives emails, judged bad from a certain number of addresses, and would like to be aware of it in order to take further decisions. Then the policy would be updated to the following

π_{3} = λx: P . x ∈ BadList ↦ [0,.5]; π_{2}(x).

At a certain stage the spam-filter could decide to add a new level of badness and create the new list VeryBadList. But at the same time it would like to change the policy with respect to BadList putting certain restrictions on the intervals which take care of other universities’ opinions.

π_{4} = λx: P . x ∈ VeryBadList↦ [0,.2]; x ∈ BadList ↦ π_{2}(x) ∧_{op}[0,.5];π_{2}(x).

As illustrated in the Spam Filter example, we see trust evolution as being modelled by suitable updates of policies, as response to e.g. observations of principal behaviour. However, it is not clear exactly what update primitives are required in practice. We are currently working on developing a calculus of principal behaviour, with features for trust policy updates, i.e. instantiating the function update introduced in §1.

Conclusion

We presented a novel model for trust in distributed dynamic networks, such as those considered in Global Computing. The model builds on basic ideas from trust management systems and relies on domain theory to provide a semantic model for the interpretation of trust policies in trust-based security systems. Our technical contribution is based bi-ordered structures (T ,⪯,⊑), where the information ordering ⊑ measures the information contents of data, and is needed to compute the fixpoint of mutually recursive policies, while the trust ordering ⪯ measures trust degrees and is used to make trust-informed decisions. Following this lead, we presented an interval construction as a canonical way to add uncertainty to trust lattices, and used the theory to guide the design and underpin the semantics of a simple, yet realistic policy language. We believe that the model can be used to explain existing trust-based systems, as well as help the design of new ones.

Of course, we are still at the first steps of development, and we still need to assess the generality of our approach is by verifying further examples. One of the main challenges ahead is to complement the denotational model presented here with an operational model where, for instance, we will need to address the question of computing trust information efficiently over the global network. Due to the great variability and absence of central control of the kind of network we are interested in, this poses serious challenges. For instance, in many applications it will not be feasible or necessary at all to compute exact values. We are therefore aiming at an operational model which can compute sufficient approximations to trust values. One issue is the update of computed trust elements; it would be interesting to investigate dynamic algorithms to update the least fixpoint. Another important issue is trust negotiation, where requester and granter engage in complex protocols aimed to convince each other of their reciprocal trustworthiness, without disclosing more evidence than necessary. Similar ideas appear in the literature as “proof carrying authentication” [1] and “automated trust negotiation” [23].

From the denotational point of view, we would like to develop a theory to account for the dynamic modification of the “web of trust.” The simplest instance of this is when a principal decides to modify its trust policy. This introduces an element of nonmonotonicity that we plan to investigate using an extension of our model based on a “possible world” semantics, where updating a policy signifies the transition to a “new world” and triggers a (partial) re-computation of the global trust function.

Acknowledgements. We would like to thank Karl Krukow and the Secure project consortium and in particular the Aarhus group and the Cambridge Opera group for the development of the research. Many thanks go to Maria Vigliotti who contributed to early developments.

References

1. Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In Proc. 6th ACM Conference on Computer and Communications Security, 1999.

2. Matt Blaze, Joan Feigenbaum, and Jack Lacy. Decentralized trust management. In Proc. IEEE Conference on Security and Privacy, Oakland, 1996.

3. Matt Blaze, Joan Feigenbaum, and Jack Lacy. KeyNote: Trust management for public-key infrastructure. LNCS, 1550:59–63, 1999.

4. Michael Burrows, Martín Abadi, Butler W. Lampson, and Gordon Plotkin. A calculus for access control in distributed systems. LNCS, 576:1–23, 1991.

5. Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication. In Proceedings of the Royal Society, Series A, 426:18–36, 1991.

6. Yang-Hua Chu, Joan Feigenbaum, Brian LaMacchia, Paul Resnick, and Martin Strauss. REFEREE: Trust management for web applications. Computer Networks and ISDN Systems, 29(8-13):953–964, 1997.

7. Dwaine Clarke, Jean-Emile Elien, Carl Ellison, Matt Fredette, Alexander Morcos, and Ronald L. Rivest. Certificate chain discovery in SPKI/SDSI. http://theory.lcs.

mit.edu/~rivest, 1999.

8. Yun Ding, Patrick Horster, and Holger Petersen. A new approach for delegation using hierarchical delegation tokens. In Communications and Multimedia Security, pages 128–143, 1996.

9. Carl M. Ellison, Bill Frantz, Butler Lampson, Ron Rivest, Brian M. Thomas, and Tat Ylonen. SPKI certificate theory. Internet RFC 2693, 1999.

10. Tyrone Grandison and Morris Sloman. A survey of trust in internet application. IEEE Communications Surveys, Fourth Quarter, 2000.

11. George Gräzer. Lattice Theory: First Concepts and Distributive Lattices. Freeman and Company, 1971.

12. Sushil Jajodia, Pierangela Samarati, and V. S. Subrahmanian. A logical language for expressing authorizations. In Proc. of the 1997 IEEE Symposium on Security and Privacy, Oakland, CA, 1997.

13. Andrew J. I. Jones and Babak S. Firozabadi. On the characterisation of a trusting agent. In Workshop on Deception, Trust and Fraud in Agent Societies, 2000.

14. Adun Jøsang. A logic for uncertain probabilities. Fuzziness and Knowledge-Based Systems, 9(3), 2001.

15. Ulrich W. Kulish and Willard L. Miranker. Computer Arithmetic in Theory and Practice. Academic Press, 1981.

16. D. Harrison McKnight and Norman L. Chervany. The meanings of trust. Trust in Cyber-Societies - LNAI, 2246:27–54, 2001.

17. Ingmar Pörn. Some basic concepts of action. In S. Stenlund (ed.), Logical Theory and Semantic Analysis. Reidel, Dordrecht, 1974.

18. P. Venkat Rangan. An axiomatic basis of trust in distributed systems. In Symposium on Security and Privacy, 1998.

19. Ronald L. Rivest and Butler Lampson. SDSI – A simple distributed security infrastructure. Presented at CRYPTO’96 Rumpsession, 1996.

20. Dana S. Scott. Domains for denotational semantics. ICALP ’82 - LNCS, 140, 1982.

21. Stephen Weeks. Understanding trust management systems. In Proc. IEEE Symposium on Security and Privacy, Oakland, 2001.

22. Uwe G. Wilhelm, Levente Buttyàn, and Sebastian Staamann. On the problem of trust in mobile agent systems. In Symposium on Network and Distributed System Security. Internet Society, 1998.

23. William H. Winsborough and Ninghui Li. Towards practical automated trust negotiation. In IEEE 3rd Intl. Workshop on Policies for Distributed Systems and Networks, 2002.

24. Philip Zimmermann. PGP Source Code and Internals. The MIT Press, 1995.

Recent BRICS Report Series Publications

RS-03-4 Marco Carbone, Mogens Nielsen, and Vladimiro Sassone. A Formal Model for Trust in Dynamic Networks. January 2003. 18 pp.

RS-03-3 Claude Crépeau, Paul Dumais, Dominic Mayers, and Louis Salvail. On the Computational Collapse of Quantum Information. January 2003. 31 pp.

RS-03-2 Olivier Danvy and Pablo E. Martínez López. Tagging, Encoding, and Jones Optimality. January 2003. Appears in Degano, editor, Programming Languages and Systems: Twelfth European Symposium on Programming, ESOP ’03 Proceedings, LNCS 2618, 2003, pages 335–347.

RS-03-1 Vladimiro Sassone and Pawe� Sobocinski. Deriving Bisimulation Congruences: 2-Categories vs. Precategories. January 2003. 28 pp. Appears in Gordon, editor, Foundations of Software Science and Computation Structures, FoSSaCS ’03 Proceedings, LNCS 2620, 2003, pages 409–424.

RS-02-53 Olivier Danvy. A Lambda-Revelation of the SECD Machine.

December 2003.

RS-02-52 Olivier Danvy. A New One-Pass Transformation into Monadic Normal Form. December 2002. 16 pp. Appears in Hedin, editor, Compiler Construction, 12th International Conference, CC ’03 Proceedings, LNCS 2622, 2003, pages 77–89.

RS-02-51 Gerth Stølting Brodal, Rolf Fagerberg, Anna Östlin, Christian N. S. Pedersen, and S. Srinivasa Rao. Computing Refined Buneman Trees in Cubic Time. December 2002. 14 pp.

RS-02-49 Mikkel Nygaard and Glynn Winskel. HOPLA—A Higher-Order Process Language. December 2002. 18 pp. Appears in Brim, Jančar, Křetínský and Antonín, editors, Concurrency Theory: 13th International Conference, CONCUR ’02 Proceedings, LNCS 2421, 2002, pages 434–448.

RS-02-48 Mikkel Nygaard and Glynn Winskel. Linearity in Process Languages. December 2002. 27 pp. Appears in Plotkin, editor, Seventeenth Annual IEEE Symposium on Logic in Computer Science, Lics ’02 Proceedings, 2002, pages 433–446.