Article · January 006 citations reads 30 authors

participating in the main protocol, if the service performs some standard negoti-
ation. Figure 3 illustrates a protocol service that exchanges messages m, m
0
with
an instance of a role r
t
. The dotted transitions indicate that the service might
go through several nodes before returning to the caller.
Ordinarily, a protocol soundness proof for a protocol that invokes a sub-
protocol would consider the protocol and subprotocol together, verifying the
composition as a single larger protocol. However, we wish to take advantage of
prior work that identifies conditions under which protocol components may be
verified in isolation, preserving their security properties when they are combined.

---

r
c c
↵◆
r
s s
r
t t
p
c c
call(x)
//
_
_
_
_
_
_
_
_
↵◆
p
s s
↵◆
m
//
↵◆
↵◆
↵◆
m
0
oo
q
c c
↵◆
q
s s
return(y)
oo_ _ _ _ _ _ _ _
Fig. 3. Protocol Service Call
Protocols may be combined in two senses. One is by refinement, which is
close to the idea of a service: a protocol needs some function accomplished, and
the objective is to prove its correctness and security while treating the function
as a black box. Then the function is later expanded into a subprotocol, which
is verified separately. One thread of research that has taken this approach with
sufficient formality and attention to security in a Dolev-Yao modeling context is
represented by Datta, et al. [6] Their composition methodology, however, requires
one to identify invariants used in the proofs of di↵erent protocol components, and
check that each component satisfies the other’s invariant as well as its own. This
approach does not, in this general form, facilitate our objective for independent
design and verification of services and the protocols using them.
Protocols are also combined, in a sense, when they are run independently
in the same attacker environment, either concurrently or sequentially. Many
papers have noted that it is possible for protocols to interfere with one another,
invalidating security properties proved in isolation, when the same principal
(using the same long-term private keys) participates in more than one protocol.
Papers on this topic, with varying degrees of formality, go back at least to [11]
and include [4] and [9]. Universal composability [3] is a strong property in the
computational arena that can also lead, for some protocols, to preservation of
security in a multiprotocol environment.
How could we use independent composition to verify services? The idea is
to treat the caller request as a pair of guarantees, rather than as a guarantee
for the precondition and a rely for the postcondition. It can then be verified
separately. The service is a separate protocol anyway, its only dependence to
the caller being the choice of input values. However, some additional conditions

---

will be necessary to prevent interference that would undermine security. Those
conditions can be reflected in the choice of NDA and its semantics.
To give an example of a particular result along these lines, we apply the pro-
tocol independence theorem from [9]. The definitions are reviewed here, though
[9] should be consulted for more details.
4.5 Review of Protocol Independence
The results concern a strand space ⌃ consisting of regular strands ⌃
1
of a pri-
mary protocol (think of this as the caller), regular strands of another secondary
protocol (from services), and penetrator strands. The following definitions are
needed.
Definition 6. A strand space ⌃ is full if every atomic value a that originates
on any secondary strand in ⌃ also originates on a penetrator strand in ⌃.
An atom a is private if it originates uniquely only in ⌃
1
.
A term t occurs in a term t
0
, written t v t
0
, if it is a subterm, but not in the
key part of an encryption. A term occurs in a node if it occurs in its message. A
component of a non-pair term is the whole term, and a pair t, t
0
has components
t and t
0
. A “new component” of a node is a term that has not occurred as a
subterm of a prior node (by )) in the same strand.
⌃ has disjoint outbound encryption if and only if the following holds. Let
n
1
2 ⌃
1
be a positive node, let n
2
2 ⌃
2
be a negative node, and let a be a
private atom occurring in some encrypted term {h}
K
, where {h}
K
<
n
1
and
{h}
K
<
n
2
. Then there is no positive n
0
2
such that n
2
)
+
n
0
2
and a occurs in a
new component of n
0
2
.
⌃ has disjoint inbound encryption if, for any negative node n
1
2 ⌃
1
and
positive node n
2
2 ⌃
2
in which an encrypted term {h}
k
occurs, {h}
k
does not
occur in any new component of n
2
.
Two bundles over ⌃ are equivalent if they have the same ⌃
1
nodes. ⌃
1
is
independent of ⌃
2
if every bundle over ⌃ is equivalent to one with no ⌃
2
nodes.
Theorem 2 (Protocol Independence, Prop. 7.2 in [9]). If ⌃ is full and has
both disjoint inbound and disjoint outbound encryption, then ⌃
1
is independent
of ⌃
2
.
The significance of protocol independence is that any attack on an authentication
property that is possible in the ⌃ multiprotocol strand space can, by equivalence,
be reproduced without ⌃
2
strands, and hence should have been excluded by a
verification of the primary protocol in isolation.
4.6 Application of Protocol Independence
The idea behind disjoint inbound and outbound encryption is that a secondary
protocol should not alter or repackage any encrypted term that either originated
in the primary protocol or could be received by it. It was observed in [9] (and

---

the idea was also suggested in other papers) that a protocol identifier could be
included in every encrypted term that was produced by a particular protocol,
so that a party that received a term encrypted by a confidential key would be
able to check that it was produced in its own protocol. All roles of the same
protocol would use the same identifier, but a di↵erent (secondary or service)
protocol would use a di↵erent identifier. Use of protocol identifiers in this way
would guarantee disjoint inbound and outbound encryption.
To apply the protocol independence theorem, we also need the “full” prop-
erty. The “full” condition requires that a confidential atom originating in the
primary protocol may not also originate in the secondary protocol. This is a
problem when the atom is passed as an input parameter to a service, since pa-
rameters that are not received in a message appear to originate in the service.
However, we can use an NDA to fix this.
If a parameter a is uniquely originating in the calling protocol, and it is
provided as an input to a service, we can list the encrypted terms in which it
occurs. Let ⌫(a) be a predicate that tests membership in that list. A service
with a compatible NDA for a parameter mapped to a recognizes a smaller list
of terms that will be mapped to the same ground terms. The semantics of the
NDA for service is the same: it specifies the set of “safe” terms in which a
confidential parameter may occur. This means that the confidential parameter
will be transmitted only in terms that can be traced back to terms originating
in the caller. The full property is then satisfied for those parameters.
The “full” condition also prevents a confidential value from being generated
by the service, since a confidential return parameter cannot be recognized as
“private”. This limits the applicability of the protocol independence result.
Note that, if we use protocol identifiers, use NDAs to limit private atom con-
texts, and refrain from generating confidential values in services to be returned
to the caller, the conditions for protocol independence apply between di↵erent
services as well as between the caller and its services.
To summarize:
Corollary 2. Under the following conditions, a calling protocol and its services
preserve authentication properties when verified independently:
1. each protocol (and service) includes a di↵erent protocol identifier in en-
crypted terms constructed by that protocol;
2. each service respects its promised NDA, in that each parameter x may occur
only in components of sent messages satisfying ⌫(x);
3. no service originates a confidential atom returned to the caller.
5
Conclusion
Call by contract is a way to specify and use interchangeable services in secure
protocols, so that protocols and services can be independently designed and veri-
fied. The interface to a service is specified with a precondition and postcondition
as in an Ei↵el contract. However, to facilitate independent design, the calling

---

protocol requests a service with its own precondition and postcondition. The
calling protocol need not know the name of the service or its parameter list.
A selection algorithm is given to test whether a candidate service is uni-
formly selectable. Uniform selection implies the existence of parameter mappings
between the caller and service such that the preconditions and postconditions
are sufficient, independently of the particular input parameter values. The se-
lection algorithm is based on a technique called abstraction binding, employing
a Datalog engine.
To facilitate independent security verification of the calling protocol and its
services, contracts and requests also provide an NDA. Informally, NDAs are
confidentiality constraints on parameters. Formally, NDAs of caller and service
are compared in a straightforward way for “secure” selectability. The semantics
of NDAs, and any proof that secure selectability enables independent verification,
are not fixed, and can be interpreted di↵erently in di↵erent protocol modeling
contexts. We have given an example of NDA semantics that yields some limited
independence, but stronger results, and di↵erent interpretations and results in
other contexts, should be possible in the future.
We have an experimental prototype implementation of the service algorithm
to support CPPL, our protocol compiler that makes use of a Datalog runtime
engine. This prototype is still under development.
References
1. M. Backes and B. Pfitzmann. Relating symbolic and cryptographic secrecy. In
IEEE Symposium on Security and Privacy, pages 171–182. IEEE Computer Soci-
ety, 2005.
2. M. Bartoletti, P. Degano, and G-L. Ferrari. Enforcing secure service composition.
In 18th IEEE Computer Security Foundations Workshop, pages 211–223. IEEE
Computer Society, 2005.
3. R. Canetti. Universally composable security: a new paradigm for cryptographic
protocols. In Proc. IEEE FOCS, pages 136–145, 2001.
4. R. Canetti, C. Meadows, and P. Syverson. Evironmental requirements for authen-
tication protocols. In Symposium on Requirements Engineering for Information
Security, March 2001.
5. Stefano Ceri, Georg Gottlob, and Letizia Tanca. What you always wanted to
know about datalog (and never dared to ask). IEEE Transactions of Knowledge
and Data Engineering, 1(1), 1989.
6. Anupam Datta, Ante Derek, John C. Mitchell, and Dusko Pavlovic. A derivation
system and compositional logic for security. Journal of Computer Security, 2005.
7. Trusted Computing Group. Trusted platform module main specification, version
1.2, 2006.
8. Joshua Guttman, Jonathan Herzog, John Ramsdell, and Brian Sni↵en. Program-
ming cryptographic protocols. In Symposium on Trusted Global Computing, volume
3705 of Lecture Notes in Computer Science. Springer, April 2005.
9. Joshua Guttman and F. Javier Thayer. Protocol independence through disjoint
encryption. In Computer Security Foundations Workshop. IEEE Computer Society,
2000.

---

10. Joshua Guttman, F. Javier Thayer, Jay Carlson, Jonathan Herzog, John Ramsdell,
and Brian Sni↵en. Trust management in strand spaces: A rely-guarantee method.
In European Symposium on Programming (ESOP), 2004.
11. N. Heintze and J.D. Tygar. A model for secure protocols and their composition.
IEEE Transactions on Software Engineering, 22(1):16–30, 1996.
12. Ninghui Li, Joan Feigenbaum, and Benjamin Grosof. A logic-based knowledge
representation for authorization with delegation. In 12th Computer Security Foun-
dations Workshop, pages 162–174. IEEE Computer Society, 1999.
13. F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces:
Proving security protocols correct. Journal of Computer Security, 7(2/3):191–230,
1999.
A
Strand Spaces: A Brief Summary
The purpose of this summary is primarily to review the vocabulary used in this
paper. It should be read to understand the latter part of Section 4.
A strand is a sequence of nodes. A node has a label (±m, ) where ±m is a
directed (+ for sent or
for received) message, and the annotation is a formula.
The atoms used in m and
are elements of the disjoint union A = X [ Z of
parameters X and values Z. The trace of a strand is its sequence of node labels.
Any sequence of node labels may be referred to as a trace. When applied to a
trace, the term “node” refers to a position in the label sequence.
A bundle is a finite partially ordered set of nodes, where each node belongs
to a partial strand (an initial subsequence of a strand) and the partial order-
ing combines the strand node sequence ordering (represented with )) and a
communication ordering ! that relates each receive node to a prior send node
with the same message. All atoms occurring in a bundle must be from Z, though
some authors make use of semibundles in which parameters may occur, and some
receive nodes do not have predecessors in the communication ordering.
A parameter is bound at a node if it occurs in the node label of that node,
or of a prior node, or (for any node) if it is an input.
A protocol is a set of roles. A role is a 4-tuple r = (R, I, U, T ) where R is a
trace in which all atoms are parameters, I is a subset of parameters designated
as inputs, U is a subset of parameters designated as uniquely originating, and
T is the initial theory. T consists of general inference rules (see Section 2) and
facts expressible as formulas over input parameters.
There are penetrator roles that define the attacker model. The penetrator
roles do not belong to any particular protocol. A penetrator role is one of a few
specific types representing the ability of the attacker to construct and decompose
messages. For example, ( k, >), ( {x}k, >), (+x, >) is a penetrator role that
performs decryption, where > is the constant true formula.
A strand is a ground strand if its atoms (the atoms occurring in its node
labels) are all values. A (strand) substitution is an idempotent map of a subset
of X into A. Strand substitutions are extended to messages, formulas, node
labels, and traces in the usual way. A strand is an instance of a role r under
substitution
if its trace is r .

---

It is a ground instance if the range of
is included in Z. A regular strand is
an instance of a protocol role. A penetrator strand is an instance of a penetrator
role.
A bundle is consistent with a protocol with roles {r
i
} if its nodes are the
disjoint union of nodesets of ground partial strands, such that each strand is
either a regular strand of some role r
i
or a penetrator strand. Furthermore, we
require that (1) each positive node formula is provable from the (mapped) initial
theory together with the formulas on prior negative nodes of the strand, and (2)
the bundle respects unique origination.
Any value of a uniquely originating parameter must be uniquely originating
in the bundle in the sense of [13]. A bundle can be consistent with a protocol
without necessarily satisfying security properties expressed as rely formulas. Pro-
tocol verification establishes correctness of rely formulas in any bundle consistent
with the protocol.
B
Implementation Notes
Notes on our implementation of the selector algorithm follow. The implementa-
tion follows the algorithm in Section 3 except that it combines the two abstraction-
binding steps into a single Datalog query. This is facilitated by adding rules
expressing the contract.
Let S( ) be a sequence of the parameters in formula . Each parameter in
S( ) occurs once, and the parameters are ordered by their first appearance in
the formula. Let V (X) be a sequence of distinct variables of the same length
as X. (V (X) can be the X-length initial subsequence of a long fixed variable
sequence.) Let r :: X be the literal constructed from predicate symbol r and the
sequence of terms X. Let p[X] be the formula in which each parameter in X is
replaced in p by its corresponding variable in V (X). Thus, p[X] is an abstraction
of p over a specific set of parameters. The concatenation of sequences X
1
and X
2
is X
1
· X
2
. The subsequence of X
1
elements that are not in X
2
is X
1
\ X
2
.
Note that, in general, a substitution
on a set X can be represented with
respect to an ordering X by a result vector Y such that (x) = Y (X
1
(x)). We
write
= Y /X. If substitutions
i
= Y
i
/X
i
have disjoint domains,
1
[
2
=
Y
1
· Y
2
/X
1
· X
2
. Also, (
⌧ )(x) = (⌧ (x)) and (
X)(i) = (X(i)).
A contract in the implementation is a 5-tuple (p
s
, q
s
, I
s
, O
s
, s), where s is
the name of the procedure that implements the service. The service contract of s
is (p
s
, q
s
), the input parameter sequence of s is I
s
, and the output parameter
sequence of s is O
s
.
A caller provides a triple (p
c
, q
c
, Z
c
), where the caller’s pre- and postcondition
are (p
c
, q
c
), and the values associated with the parameters in S(p
c
) are given
by Z
c
. Thus,
e
= Z
c
/I
c
for I
c
= S(p
c
). A call is ill-formed if the length of Z
c
di↵ers from the length of I
c
. Let O
c
= S(q
c
) \ S(p
c
).
If the selector algorithm determines that a service s is selectable, and then
selects it, it invokes the service with a sequence of input values Z
s
and a sequence

---

of natural numbers N
s
. The sequence N
s
is defined below; it tells the service
which values to return, and in which order, corresponding to caller outputs.
The selector algorithm is the following.
1. Rename parameters in the service contract to ensure that service parameters
do not occur in caller’s formulas.
2. Assert each literal in p
c
.
3. Recall that a formula is a conjunction of literals, and let
i
be the i-th literal.
For each literal in q
s
[I
s
], assert q
i
s
[I
s
] :- p
s
[I
s
]. If any clause is not safe, the
service s is not selectable. These rules represent the contract.
4. Let r be a fresh predicate symbol. Assert r::V (I
s
·O
c
):-p
s
[I
s
·O
c
], q
c
[I
s
·O
c
].
If the clause is not safe, the service s is not selectable.
5. If an instance of r :: V (I
s
· O
c
) is derivable, the service s is selectable.
Let r :: I
s
· O
c
be a derived instance of r :: V (I
s
· O
c
). The input values Z
s
required by the service are obtained as (Z
c
/I
c
) (I
s
/I
s
) I
s
. The number
sequence N
s
given to the service is obtained as (I
s
· O
s
)
1
O
c
.
The service then executes and produces its own output values Z
o
. It then
produces the sequence of values for caller outputs as Z
s
· Z
o
N
s
.
View publication stats
View publication stats