Article · January 006 citations reads 30 authors

---

See discussions, stats, and author profiles for this publication at: 
https://www.researchgate.net/publication/237129622
Call by Contract for Cryptographic Protocols?
Article
· January 2006
CITATIONS
3
READS
30
5 authors
, including:
Some of the authors of this publication are also working on these related projects:
Virtual Library of Babel
 
View project
Cryptographic Protocol Analysis
View project
Jonathan Millen
87
PUBLICATIONS
2,946
CITATIONS
SEE PROFILE
Joshua D. Guttman
MITRE
133
PUBLICATIONS
4,327
CITATIONS
SEE PROFILE
John D. Ramsdell
MITRE
56
PUBLICATIONS
610
CITATIONS
SEE PROFILE
Justin Sheehy
8
PUBLICATIONS
205
CITATIONS
SEE PROFILE
All content following this page was uploaded by 
Justin Sheehy
 on 14 March 2017.
The user has requested enhancement of the downloaded file.

---

Call by Contract for Cryptographic Protocols
?
Jonathan Millen, Joshua Guttman, John Ramsdell,
Justin Sheehy, and Brian Sni↵en
The MITRE Corporation
Bedford, MA 01730
USA
jmillen,guttman,ramsdell,justin,[e-mail]
Abstract. Call by contract is a way to specify and use interchangeable
services in secure protocols, so that protocols and services can be inde-
pendently designed and verified. A selection algorithm is given to test
whether a candidate service is uniformly selectable. To facilitate inde-
pendent security verification of the calling protocol and its services, con-
tracts and requests also provide an NDA (Non-Disclosure Agreement).
Informally, NDAs are confidentiality constraints on parameters.
1
Introduction
A compositional approach to protocol design and analysis is recognized as ad-
vantageous. We wish to perform design decomposition in a way that permits
independent design and verification of components, and preserves security and
correctness goals when the components are recombined. There are many di↵erent
ways in which composition can be interpreted and implemented. Our version of
composition applies to the design of secure protocols. Our objective is to extend
verification techniques based on abstract encryption models to protocols that
incorporate or implement encapsulated services.
One use for such services is to invoke computations that are not included
in the vocabulary of operations built into the protocol specification language,
such as the special operations of a Trusted Platform Module [7] or some other
specialized cryptographic application interface. Another use is to allow flexibility
in the choice of means to implement an operation. For a public-key lookup, for
example, there may be two alternative services, one that fetches a locally cached
certificate, and another that initiates a protocol with a directory server to retrieve
one. A service might even establish a shared session key between two parties who
have already begun a protocol.
With encapsulation of services, we can create and maintain a library of ser-
vices that could be shared by all protocol processes running on the same system.
The service library can be updated with improved implementations without dis-
turbing existing protocols, and new services can be added at any time for use
?
This work was supported by the National Security Agency through US Army CE-
COM contract W15P7T-05-C-F600.

---

by future protocols. New services can also be used by older protocols if they
extend older services, that is, if their functionality is more general or their input
requirements are less strict.
There are two challenges in designing and using services: first, to allow for
use of services whose specific interfaces have not been anticipated; second, to
assure ourselves that it is safe to use separately designed services when there are
security as well as functionality concerns.
Our “encapsulated services” should be distinguished from “Web services” be-
cause they can be purely local. Furthermore, the security objectives that we wish
to protect are the traditional confidentiality and authentication goals for secure
protocols, rather than the more specific access control, execution history [2] or
other policies associated with Web services. However, we need not exclude Web
services as an option for implementing an encapsulated service. Our focus is on
the interface to a calling protocol and on maintaining the security objectives of
that protocol.
Service specifications will be expressed in a logical call-by-contract form. An
algorithm for selecting services that satisfy protocol requests is given. We take
into consideration that a service specification may include not only functional
guarantees but also confidentiality guarantees, which we call non-disclosure agree-
ments (NDAs). We give some conditions under which authentication and secrecy
properties established in a Dolev-Yao idealized encryption context can be carried
over to a general service invocation context.
In the remainder of this section, the formal modeling context is presented.
Then, in Section 2, we give the abstraction-binding technique that underlies
the selection algorithm. In Section 3, we show how abstraction binding is used
to select services in response to requests. In Section 4, we investigate how the
conventional Dolev-Yao techniques for verification of protocol security can be
extended safely to this more general context.
1.1 Modeling Style
Protocols are modeled here as sets of roles, where a role is the trace of a parame-
terized annotated strand. An annotated strand, as presented in [10], extends the
basic strand notion from [13] by labeling nodes not only with messages but also
trust management formulas. The vocabulary used in this paper is reviewed in
Appendix A. Most of the details are not necessary until we apply a prior strand
space result in the latter part of Section 4.
Messages in this model are elements of a free message algebra, presented
as expressions constructed from atoms of a few sorts (such as key and text)
and operators such as idealized encryption and pairing. Formulas are logical
expressions over the same set of atoms. The threat environment is a version of
the Dolev-Yao attacker model, in which there is a single attacker who is assumed
able to intercept any message, and able to decompose or construct messages
using the available operators, but unable to encrypt or extract information from
encrypted messages without the appropriate key. Models of this kind have been
widely used to analyze the vulnerability of protocols to attacks such as replay

---

and spoofing, in which the attacker fools an honest participant into revealing
an entire key or accepting a key provided by, or previously compromised by, the
attacker.
1.2 Trust Management Formulas
The germ of the call-by-contract idea was presaged in the rely-guarantee trust
management approach described in [10]. The trust management formula associ-
ated with a positive (send) node is a guarantee, expressed in terms of the protocol
parameters, that must be provable for the values bound to those parameters. The
formula associated with a negative (receive) node is a rely formula, which may be
assumed in proofs of subsequent guarantees. The local theory of a node consists
of the initial theory T plus the rely formulas of prior nodes in the role. Rely
formulas are authentication goals whose validity must be proved by the protocol
designer as part of the verification of the protocol.
Note that guarantees can be active, in the sense that they bind parameter
values. For example, a guarantee pubkey(a,ka) may be evaluated in a node
prior to which the parameter a is bound but ka is unbound, and its e↵ect is to
look up the public key of principal a in the local theory and bind ka to it.
1.3 General Services
A service can be viewed as a guarantee that is provided by a separate role of the
same principal, like a subprotocol. This view is illustrated in Fig. 1. A calling
strand invokes the service with a call that guarantees some precondition formula
that implies the service precondition ⇢
0
, and the service strand sends a return
annotated with another formula
0
that is the service postcondition, which should
imply the caller’s desired rely condition ⇢. The call and return messages convey
the sequences of values of the input and output parameters respectively. Call and
return operators could be modeled as additional operators in the free algebra
which create private messages, in the sense that they are neither constructible
nor analyzable by the attacker. (They could also be modeled using the special
protected message directions introduced in [8].)
A service has a precondition and postcondition, as in the terminology of the
Ei↵el “design by contract” concept. Our focus, however, is not on how the service
implements its contract, but rather on how a service selection mechanism can
adapt a caller rely formula ⇢ to a di↵erent but sufficient service postcondition
0
that was stated with a di↵erent set of formal parameters. We also need to match
the caller guarantee to the service precondition.
A service is selectable for a call request if there exists a parameter mapping
that assigns values to service inputs from caller inputs, and caller outputs from
service outputs, such that the service precondition and the caller postcondition
are both satisfied.
For example, suppose that the caller requirement has certAuth(z) as a pre-
condition, and its postcondition is pubKey(a,ka), so that its parameter set is
P
c
= {a,ka,z}. The caller has bound a and z and needs a value for ka. It might

---

Caller
↵◆
Service
call(x)
//
_
_
_
_
_
_
_
_
_
_
↵◆
⇢
0
↵◆
⇢
↵◆
0
return(y)
oo_ _ _ _ _ _ _ _ _ _
Fig. 1. Calling a service
be satisfied by a service that asks for the precondition certAuth(ca) and o↵ers
the postcondition pkCert(pk,p,ca), and its parameters are P
s
= {pk,p,ca},
where ca is a certification authority. To match the service to the call, we must
find the mapping p 7! a, ka 7! pk, and ca 7! z. This match is justified using an
inference rule like:
pubKey(A,K) :- pkCert(K,A,C), certAuth(C).
This rule is presented in the Horn clause format used in Datalog and Prolog,
for reasons given in the next section. The capital letters used as arguments are
logical variables.
Where does this inference rule come from? We assume that there is a selector
theory with conversion rules useful for translating between caller and service
predicate vocabularies.
At this point it is possible to point out the di↵erences between the service idea
and the prior related concepts of guarantees and subprotocols. First, guarantees
are established logically, by inference from the caller’s local theory, while the
mechanism by which a service establishes its postcondition is not specified. A
service postcondition might result from any computation, or from a separate
protocol.
A service is di↵erent from a subprotocol because it might just be a local
computation, but even when it is a protocol, the calling mechanism is di↵erent.
A subprotocol call identifies a subprotocol with a known name and parameters,
while our services are selectable through a flexible matching mechanism that can
search through a list of many subprotocols to find one that can be made to fit
through a suitable parameter mapping.
1.4 Non-Disclosure Agreements
One way in which Fig. 1 is incomplete is that it does not show that the ser-
vice may participate in a protocol that communicates with other principals.

---

Parameter values that it shares with the caller might be transmitted in proto-
col messages. A caller might want to insist that some shared parameter values
be kept secret, either by not sending them out at all, or by sending them only
to (strands owned by) some designated principals. Specifications of this kind
must be provided by the caller requirement and by the service contract. Our
formulation of this kind of specification is an “NDA” and it will be discussed in
Section 4.
2
Abstraction-Binding Inferences
Our objective is not merely to define the call-by-contract relationship, but also
to describe a practical way to implement the selection mechanism that matches
services to requests. The selection mechanism takes advantage of Datalog, be-
cause we have already been using Datalog to support the rely-guarantee trust
management approach. It has been implemented as part of the runtime system
for a high-level protocol programming language, CPPL [8].
Datalog is a restricted form of first-order logic in which each formula is a
function-free Horn clause, and every variable in the head of a clause must appear
in the body of the clause. A clause that meets this condition is called a safe
clause.
Datalog [5] forms the foundation of many deductive database systems, as
well as at least one trust management language [12]. A Datalog literal has the
form predicate-symbol(t
1
, ..., t
k
), where each argument t
i
is either an arity-zero
function symbol (i.e., a constant) or a logical variable. The predicate symbols and
constants are application-specific, and begin with lower-case letters. Variables
begin with capital letters. In Datalog, a theory is a set of safe Horn clauses of
the form head :- body where the head is a literal and the body is a (possibly
empty) sequence of literals. A clause with an empty body is a fact, and a clause
with at least one literal in the body is a rule.
The conditions on asserted clauses guarantee that the set of all facts that can
be derived from a Datalog theory is finite, and there is a terminating algorithm
to find all provable instances of a given literal presented as a query. This is the
essential feature of Datalog for our purposes.
In order to apply Datalog to node formulas, we restrict ourselves to formulas
that are expressible as conjunctions of Datalog ground literals. We use Datalog
constants to represent atoms, both parameters and values. Thus, principal sym-
bols such as p, a, ca and key symbols like pk, ka appear in literals as atoms,
and are used as arguments of predicates such as pubKey and certAuth.
To apply the Datalog engine, we may abstract a formula by replacing some
or all of its parameters with fresh, distinct variables. Other atoms are left un-
changed. The abstraction step can be represented with a substitution ↵, with a
domain given in context.
Now, suppose p and q are formulas, and T is a theory consisting of a set of
rules. We wish to check whether some instance of q follows from p in the context

---

of T . For now, assume that q is a single literal. The Datalog engine is used as
follows:
1. assert T and p;
2. present the abstracted literal q↵ as a query.
The engine will either fail (if no instance of q↵ is provable), or it will find all
variable bindings
such that q↵ is provable from T and p, that is,
T, p
` q↵ .
If we let
= ↵ , we see that we have found a substitution
of parameters
into values such that
T, p
` q
The combination of these two steps is abstraction binding.
Recall that A = X [C, and let A( ) be the set of atoms occurring in formula
. Also let A(T ) = S{A( )| occurs in T }. Abstraction binding has the following
property:
Proposition 1. Let T be a constant-free theory, consisting of rules such that
A(T ) =
;, and let p and q be formulas. Then abstraction-binding finds the set of
all substitutions
on A(q) \ A(p) into A(p) such that T, p ` q .
If q is a conjunction, we can achieve the same result by satisfying its conjuncts
sequentially, extending
as needed. (One way to do this is to introduce a new
predicate name for q, and add a rule for it with the conjuncts of q serving as the
body.)
For convenience, we define the abstraction-binding AB relation as follows:
Definition 1 (Abstraction Binding). AB (T, p, q, ) i↵ is a substitution on
A(q)
\ A(p) into A(p) such that T, p ` q .
AB relations are preserved by precondition substitutions.
Proposition 2 (AB Substitution). If AB (T, p, q, ) and ⌧ is a substitution
on A(p), then AB (T, p⌧, q, ⌧).
This conclusion is valid because T is constant-free, so the inference cannot de-
pend on particular choices for the parameters of p. The parameters of p are like
Skolem constants, since they do not occur in T . An inference that holds with
them can be generalized to a universal statement about variables in their places,
which are given values by ⌧.
3
Selection: Call by Contract
In this section we begin by looking at a static specification of a successful ser-
vice call. In a protocol with a service call, the service role is represented by an
idealization of the service, in which only the initial and final nodes are present,
as in Figure 1. A bundle containing a service call instantiates the caller role r
c

---

with some ground substitution
c
, and the idealized service r
s
with a ground
substitution
s
, which is defined only on the service parameters named in the
contract.
A request from a caller has a precondition formula p
c
and a postcondition
formula q
c
. Each service has a precondition p
s
and a postcondition q
s
. With
the substitutions and the condition formulas just defined, Figure 1 turns into
Figure 2.
r
c c
↵◆
r
s s
Caller
Service
p
c c
call(x)
//
_
_
_
_
_
_
↵◆
p
s s
↵◆
p
c c
↵◆
+3
p
s s
↵◆
q
c c
↵◆
q
s s
return(y)
oo_ _ _ _ _ _
q
c c
q
s s
ks
Fig. 2. General service diagram (a) and implications (b)
In Fig. 2(a), the input and output conditions do not have to match exactly,
but we want them to satisfy the implications summarized in the diagram (b).
For any service, we assume that it satisfies its contract, expressed as a pre-
condition, postcondition pair (p
s
, q
s
). The contract assumes that the service has
been called with an assignment of values to input parameters, which are the pa-
rameters in p
s
. If p
s
holds with these values, the contract promises to find values
for the output parameters (the parameters in q
s
that are not input parameters)
to satisfy q
s
.
Notation. For a precondition, postcondition pair (for either a service or a caller),
it is convenient to introduce symbols for its input parameters I = A(p), its output
parameters O = A(q) \ A(p), and all of its parameters P = I [ O. Subscripts s
or c will be applied as needed in context.
Definition 2. A service contract is a pair of node formulas (p
s
, q
s
) such that
P
s
✓ X and, for all
on I
s
into Z,
p
s
) (9⌧) q
s
⌧
where ⌧ is on O
s
into Z.
Definition 3. A service contract (p
s
, q
s
) is independently selectable for caller
request (p
c
, q
c
) if, for any input substitution
e
: I
c
! Z, there exist substitutions
c
: P
c
! Z extending
e
and
s
: P
s
! Z such that

---

1. T, p
c c
` p
s s
,
2. p
s s
) q
s s
, and
3. T, q
s s
` q
c c
.
The qualifier “independently” reflects the condition that the same service is
selectable regardless of which input substitution is chosen. Non-independent se-
lectability would mean that a service is selectable for some inputs but not others.
With a constant-free selector theory, we shall see that independent selectability
is not only possible, but it can be checked as soon as the service contract and
caller protocol are known.
3.1 From the Static to the Algorithmic View
The Selection Theorem shows how selectability can be established via two abstraction-
binding steps.
Theorem 1 (Selection). Let T be a constant-free theory, and suppose that
p
c
, q
c
, p
s
, q
s
are node formulas such that P
c
is disjoint from P
s
. Assume that
1.
e
: I
c
! Z,
2. (p
s
, q
s
) is a service contract,
3. AB (T, p
c
, p
s
,
i
), and
4. AB (T, q
s i
, q
c
,
o
).
Then (p
s
, q
s
) is independently selectable for (p
c
, q
c
). Furthermore, there exists a
substitution
r
: O
s
! Z such that T, p
c e
` q
c o e r
.
Proof. We will find
r
: O
s
! Z from which we construct
c
=
o e r
and
s
=
i e r
. The diagram may help in tracing the substititions.
O
c
o
//
o
✏✏
O
s
r
✏✏
I
s
i
// I
c
e
// Z
We apply the contract once and AB Substitution twice. Hypothesis 3 implies
that
i
: I
s
! I
c
, and hypothesis 4 implies that
o
: O
c
! P
s
.
Applying hypothesis 3 with
e
: I
c
! Z, we get AB (T, p
c e
, p
s
,
i e
) by
AB substitution. This means that T, p
c e
` p
s i e
. By construction, the first
condition T, p
c c
` p
s s
is satisfied (since p
c
and p
s
have no outputs). Applying
the contract in hypothesis 2, we produce
r
: O
s
! Z such that q
s i e r
holds.
This satisfies the second condition p
s s
) q
s s
by construction.
By AB substitution on hypothesis 4 with
e r
, we find that T, q
s i e r
`
q
c o e r
. This gives us T, q
s s
` q
c c
.
u
t
The Selection Theorem gives us more than just independent selectability, since
it shows that the caller and service substitutions can be factored through input
and output mappings
i
and
o
. This turns out to be important later when we
consider confidentiality constraints. The following definition names this result.

---

Definition 4. A service contract (p
s
, q
s
) is uniformly selectable for caller request
(p
c
, q
c
) if, for any input substitution
e
: I
c
! Z, there exist substitutions
i
: I
s
! I
c
and
o
: O
c
! P
s
such that independent selectability is satisfied by
c
=
o e r
and
s
=
i e r
for some
r
: O
s
! Z.
Corollary 1. Under the conditions of the Selection Theorem, (p
s
, q
s
) is uni-
formly selectable for (p
c
, q
c
).
The contract selection algorithm implied by the Selection Theorem is to consider
each available service contract (p
s
, q
s
). To test acceptability of a contract, apply
abstraction binding to find
i
, and if successful, apply abstraction binding again
to find
o
. If successful again, the service is selectable. Backtracking or other
search methods can explore multiple candidates for
o
and
i
. If none work,
other contracts are tested.
Note that all of this can be done without knowing
e
. At run time, the service
is invoked with the input substitution
i e
. When the service completes, caller
outputs are bound with
o e r
.
When multiple (
i
,
o
) solutions exist, application preferences or constraints
can be used to guide the search order or otherwise choose among alternative
call mappings. The contract selection algorithm as stated does not yet consider
security constraints, which are discussed in the next section.
4
Separate Verification of Protocol Services
Our objective is to separate the verification as well as the design and specification
of services from that of calling protocols. We need to investigate the conditions
under which this is possible. In this section we provide some preliminary issues
and answers, though more research is advised to obtain broader results.
In the context of the strand space approach, we are concerned with authen-
tication goals, as expressed in protocol rely formulas, and confidentiality goals,
either for their own sake, or to support authentication proofs.
Some issues regarding information flow are discussed first, then the general
question of protocol separation is considered.
4.1 Information Flow Through Services
The implementation of a service could a↵ect the soundness of the protocol, if
it violates confidentiality assumptions. We need to know that the computation
implementing a service does not cause information flows from a secret input
parameter to an unprotected output parameter.
For example, suppose that a protocol role has a uniquely originated, fresh,
random nonce k that we want to keep secret. And suppose there is a service
with contract (true, copy(a,b)), where copy(a,b) does what it says, namely
to bind b to the value of a. If this service is called to obtain a postcondition
copy(k,m)
, and then the caller sends m as a message, the nonce k has obviously
been compromised.

---

If copy were just a predicate used as a guarantee, this problem would surface
routinely. The behavior of copy would have to be defined in the local theory. The
theory would include a rule like A = B :- copy(A,B), and any decent security
analysis would notice the consequences.
However, a copy service might be selected for a caller whose local theory did
not even possess an equality predicate. The caller might only have requested a
weaker postcondition like same length(k,m).
To use services safely, then, we need to provide a way for the caller to spec-
ify confidentiality constraints, and for services to advertise their confidentiality
promises. We also need a way to verify such promises, and to establish that the
constraints are sufficient to preserve the security properties of the caller.
Protocol analysis based on computational models can determine whether ser-
vices computed algorithmically leak significant partial information, even when
they do not actually lead to an equality relation. This kind of analysis is dis-
cussed, for example, in [1]. In this paper, we just point out that such techniques
exist, and our discussion on verifying confidentiality will focus on protocols and
subprotocols.
4.2 NDAs
As mentioned in Section 1.4, a confidentiality requirement or contract is ex-
pressed as an NDA (non-disclosure agreement). An NDA associates a predicate
on message terms with each parameter of a role. The NDA ⌫(x) of a parameter
x expresses a constraint on the way x may be released. The predicate formula is
not necessarily restricted to the language of node formulas.
In this subsection, we leave open the semantics of ⌫(x). The way in which
an NDA is used will be presented, at first, just formally, and then in the next
subsection we provide a particular interpretation that justifies some security
conclusions.
Definition 5. A secure service request is a 4-tuple (p
c
, q
c
,
e
, ⌫) of a caller pre-
condition, a caller postcondition, an input value substitution, and an NDA de-
fined on the caller parameters P
c
. A secure service contract is a triple (p
s
, q
s
, ⌫)
where ⌫ is defined on the service parameters P
s
.
The contract (p
s
, q
s
, ⌫) is securely selectable for (p
c
, q
c
,
e
, ⌫) if it is uniformly
selectable with parameter mappings
i
,
o
and
(1) if x 2 I
s
then ⌫(x)
i
) ⌫(x
i
)
o
and
(2) if y 2 O
c
then ⌫(y
o
)
i
) ⌫(y)
o
.
Condition (1) says that the constraint on a service input is stricter than the
constraint on the caller input to which it maps. Condition (2) says that the con-
straint on a service output is stricter than the constraint on any caller parameter
mapped to it.
The parameter mappings applied to the ⌫ sets are necessary to make them
comparable. This is easy to understand if one considers the way terms are

---

mapped to values. With uniform selection, a caller term t gets the value t
c
=
t
o e r
, and a service term t
0
gets the value t
0
s
= t
0
i e r
. So if t
o
= t
0
i
then t and t
0
are mapped to the same value.
4.3 Example: Binary NDA
Suppose that ⌫(x) is either true, meaning that x is releasable without restriction,
or false, meaning that x may not be released at all. There is a trivial service
contract (nonce(x), nonce(x)), and a selector rule copy(A,A) :- nonce(A).
The secure service request is (nonce(a), copy(a,b),
e
, ⌫) where
e
is arbitrary
and ⌫(a) = ⌫(b) = false. Note that I
c
= {a}, O
c
= {b}, I
s
= {x}, and O
s
= ;.
What should the NDA of the service be?
First, observe that the service is uniformly selectable with x
i
= a and
b
o
= x.
Applying the parameter mappings, the secure selectability conditions become
(1) ⌫(a)
i
) ⌫(a)
o
and
(2) ⌫(x)
i
) ⌫(b)
o
.
Now apply the ⌫ values for the caller. Condition (1) is just false = false.
Condition (2) is ⌫(x)
i
= false. Hence we need ⌫(x) = false. The service is
being required to keep its input confidential.
There is a way to enforce binary NDA checking for free through the basic
functional selection mechanism. For each caller input x such that ⌫(x) is true,
add to the initial theory the assertion public(x). And if ⌫(x) is false, add the
assertion hidden(x). Now, for both caller and service, all public assertions are
added as conjuncts to preconditions, and all hidden assertions are added as
conjuncts to postconditions. Thus, if a service treats an input as public, that
will automatically be justified, as part of the selectability check, by checking
that the caller input it maps to is public; and if a caller believes that an output
is hidden, that will be justified by checking that the service treats the parameter
it maps to as hidden.
4.4 Services Implemented as Protocols
Many useful services are implemented as protocols that exchange messages with
a third party. For example, a service might check certificate revocation by con-
tacting a validation authority. The “third” party might also be a party already