Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL - Computer Network Security - page 39

We write M,w | = ϕ provided that w ∈E M [[ ϕ ]]. We write M| = ϕ provided that

M,w 0 | = ϕ ; this relationship is pronounced “ M satisfies ϕ ”. Finally, we say that

ϕ is valid (and write satisfy ϕ .

The logical rules of Figure 1 are sound with respect to the Kripke semantics:
for every formula ϕ ,

| = ϕ ) if all Kripke structures M

= ϕ . Therefore, every formula that can be
derived from the logical rules is satisfied in all Kripke structures.

ϕ implies that |

4 CORBA Example in the Calculus

We now return to the online-banking scenario introduced in Section 2, changing
the names of the actors for expository purposes:

A banking customer Bob uses a web browser to access his online banking
account to pay a bill. The web browser (WB) requires Bob to give his
username and password (

), which the browser passes along
with Bob's bill-payment request ( r ) to the online-banking server (S) via
a CORBA CSIv2 request.

Bob, pwd

In terms of Table 1, WB is playing the part of Tony (i.e., a transport principal
who uses SSL), and Bob is cast as Clyde (i.e., the client-authentication field
contains Bob's userid and password). The online-banking server is the target
service provider, and thus serves as Carol. If we assume that there is no identity
token included with the request, then this scenario again conforms to the fourth
case of the table.
The banking server interprets the request as two pieces of information:

says says r

WB Bob (1)

WB says ( Bob, pwd speaks for Bob ) (2)

Thus, from the banking server's perspective, WB is making two claims: (1) that
Bob wants to perform action r , and (2) that the username-password pair belongs
to Bob.
Now suppose that banking server has an access-control policy that allows
WB

for S Bob to perform the action r : that is, r can be performed only if S de-
termines that WB is working on Bob's behalf. In the Abadi calculus, WB for Bob

is syntactic sugar for a principal WB Bob , where D is a (fictional) dele-

gation authority. In an open system, however, there may be several such (possibly
nonfictional) authorities. Thus, we generalize this approach by subscripting the
for

| Bob ∧ D |

operator with the name of a specific authority, in this case the banking server
S itself.
The online-banking server is prepared to believe that WB is working on
Bob's behalf, provided that its trusted password server ( PS ) verifies the pair
Bob, pwd

. Thus, the banking server is governed by the following rule:

(( WB ∧ PS ) says ( Bob, pwd speaks for Bob ))

⊃ ( WB |Bob ) speaks for ( S|Bob ) (3)