The rigorous incremental development of security protocols has so far received much less attention than protocol verification techniques. In this work, we study security protocol transformations. These can serve both for simplifying protocols before verification and, in the other direction, for developing protocols by stepwise refinement of simple abstract protocols into complex concrete ones. The transformations preserve attacks on a class of security properties. Our work aims to improve our understanding of modifications of existing protocols and to enable the systematic development of entire families of new protocols. This complements existing work on post-hoc protocol verification.
It is well-known that security protocols are notoriously hard to get right. This motivates the use of formal methods for their design and development. In the last decade, we have witnessed substantial progress in the formal verification of security protocols. However, methods for developing security protocols have received much less attention and protocol development remains more an art than a science.
Sprenger and Basin [
This motivates our study of refinements in terms of protocol transformations at the
level of cryptographic messages. In particular, we are interested in protocol
transformations that preserve attacks against a given set of security properties from concrete
protocols to abstract ones (or, equivalently, the satisfaction of such properties in the
reverse direction). Such transformations can serve the systematic development of
individual protocols and entire families of protocols. Moreover, they can be applied to modify
or compare existing protocols and understand their di erences. The modification of
security protocols is particularly error-prone (see, e.g., [
Security protocol transformations can also be considered as abstractions (i.e., from
concrete to abstract). Hui and Lowe [
Datta et al. [
Guttman [
The objective of our work is to develop a comprehensive theory of protocol
transformations covering a wide range of protocols and security properties. Our starting point
is Hui and Lowe’s work [
We intend the following contributions. We want to significantly extend the scope of existing work in terms of expressiveness of the protocol specifications, the protocol transformations, and the preserved properties. Our work will provide a sound formal underpinning to protocol transformations, which can serve as a foundation for rigorous security protocol development, modifications, and comparisons of existing protocols. 2
We present the development of a key transport protocol as a motivating example. We state the protocols in standard Alice&Bob notation and describe each refinement step as a protocol transformation.
Consider a key transport protocol P1, where a key server S generates and distributes a session key KAB to an initiator A and a responder B.
M1.1. A ! S : A; B M1.2. S ! A : fB; KABgKAS
M1.3. S ! B : fA; KABgKBS
In order to prevent replays and guarantee the recentness of KAB, we refine this protocol into P2 by adding a nonce and a timestamp to P1.
M2.1. A ! S : A; B; NA M2.2. S ! A : fB; TS ; NA; KABgKAS
M2.3. S ! B : fA; TS ; KABgKBS Next, we obtain P3 by refining the flow of protocol messages: the server now appends B’s message in M2.3 to A’s in M2.2, which A then forwards to B.
M3.1. A ! S : A; B; NA M3.2. S ! A : fB; TS ; NA; KABgKAS ; fA; TS ; KABgKBS
M3.3. A ! B : fA; TS ; KABgKBS In P3, B cannot be sure that A has received the key KAB. We refine P3 into P4 by having the server encrypt B’s message inside A’s, which allows A to authenticate B on KAB.
M4.1. A ! S : A; B; NA M4.2. S ! A : fB; TS ; NA; KAB; fA; TS ; KABgKBS gKAS
M4.3. A ! B : fA; TS ; KABgKBS Protocol P4 is a basic form of the Kerberos IV protocol (without authenticators). We have started from a simple initial protocol guaranteeing only the secrecy of the session key. We have then used refinement to add several features to this protocol in order to obtain key freshness, recentness, and authentication properties.
For additional examples of protocol developments, we refer the reader to [
Security protocol model We briefly summarize our security protocol model, which
is based on [
We specify protocols as finite sets of roles instead of the informal Alice&Bob notation from Section 2. Each role R 2 Role is a sequence of send and receive events of the form snd(t) or rcv(t) for a term t. The semantics of a protocol is a transition system with states of the form s = (tr; th; ), where tr is a trace consisting of a sequence of pairs of thread identifiers and events, th : T ID * Role is a thread pool, and = f i j i 2 dom(th)g is a family of ground substitutions i, one for each thread i. The transitions are defined by an operational semantics with rules for sending and receiving messages. The receive rule includes a premise requiring that the received message is deducible by the intruder from his initial knowledge and the sent messages. We write R(P) for the set of reachable states of the protocol P.
Protocol transformations Our protocol transformations are functions f : T ! T on terms, which we lift to events, roles, protocols, traces, and states. We consider a class of nice transformations, which includes the following operations on messages: 1. remove encryptions and hashes, 2. remove fields from an encrypted message, 3. pull fields outside of an encryption, 4. split encryption into several ones, and 5. project pairs (under certain conditions) and reorder pairs.
T ` u ) f (T ) ` f (u)
These protocol transformations simplify messages (and hence protocols) and can therefore be understood as abstractions. However, the same transformations can be used for protocol refinements, which proceed in the opposite direction, from abstract to concrete. For example, in Section 2, the refinement of P1 into P2 uses transformations of the second type, and the one from P3 into P4 uses a transformation of the third type.
So far we do not cover structural transformation of protocol like the message relaying transformation (cf. the refinement of P2 to P3), but we plan to do so in the future. Property specification language We consider a property specification language with formulas of the following shape. The quantifiers range over thread identifiers and , are sets of atomic predicates. These predicates include learns(m) for expressing intruder knowledge in secrecy properties, and event orderings e e0 and equations m = m0 for authentication properties. To achieve attack preservation, the learns(m) is only allowed to occur in . A state s = (tr; th; ) that does not satisfy a property , written s 6j= , is called an attack on . Attack preservation Suppose we are given a class of security protocols, properties, and transformations such as those sketched above. The main result we want to achieve is the preservation of attacks on a property of protocol P to attacks on the transformed protocol f (P) and property f ( ). We formalize this property as follows. 8(tr; th; ) 2 R(P): (tr; th; ) 6j= ) ( f (tr); f (th); f ( )) 2 R( f (P)) ^ ( f (tr); f (th); f ( )) 6j= f ( ) (2) We decompose the proof of such results into two parts: the preservation of (i) executability (first conjunct) and (ii) attacks (second conjunct).
Executability The proof that for each reachable state (tr; th; ) of P the transformed state ( f (tr); f (th); f ( )) is reachable in f (P) is based on the following deducibility preservation result.
T ` u
) f (T ) f ( ) ` f (u) f ( ) This follows from two simpler properties. The first one is a simpler version of (3). (1) (3) (4)
The second one requires that f satisfies the following substitution property, that is, for all terms t and substitutions , f (t ) = f (t) f ( ) (5) In particular, since the operational semantics of receive events requires the deducibility of the received message from previously sent messages, we can use (3) to show that each receive event of P can be simulated by a corresponding receive event in f (P). Attack preservation Since secrecy is expressed in terms of deducibility of messages, we obtain the preservation of secrecy for free from the above. For other properties, like those expressible in the language sketched above, a separate proof is needed.
We have proved property (4) for all nice transformations. However, the
substitution property (5) turns out to be quite restrictive. It rules out transformations that look
more than one level into the term structure (such as, e.g., for splitting an encryption).
Our initial solution restricts the set of substitutions to simple ones, whose range
contains no composed terms. This set covers typed substitutions, which are (implicitly)
used in [
Generalizing the results An alternative solution is based on the observation that executability depends on constraints T ` u where the terms in T stem from send events and u from a receive event. Therefore, a restricted form of (5) where t ranges over the set of terms in the protocol roles su ces for executability. Since this form of (5) is protocoldependent, we cannot use induction to establish it. Instead, we need to formulate criteria to check that a protocol has this property. For attack preservation, the substitution property must also hold for the terms occurring the properties we are interested in.
A di erent approach could replace the substitution f ( ) in (3) by some 0. The
construction of such a 0 would require a stronger proof technique, possibly based on
symbolic constraint reduction [
Outlook on future work In a longer-term perspective, we plan to extend the scope of
transformations in several directions. First, we want to cover structural transformations,
which not only modify messages, but also events and roles (e.g., relaying messages;
splitting, merging, and deleting events). Second, we would like to cover a larger class
of protocols, in particular, by including equational theories (e.g., Di e-Hellman
exponentiation, convergent subterm theories [
Conclusions In this work, we study attack-preserving security protocol transformations. These can be used for the abstraction, the refinement, and the comparison of protocols. Therefore, we consider this technique as a useful complement to verification.
So far, we have defined a subclass of transformations and proved the preservation of attacks with respect to a particular security property language. We have discussed the problems that we have encountered and proposed possible solutions. We have also sketched our plans for future work.
Acknowledgements This work is partially supported by the EU FP7-ICT-2009.1.4 Project No. 256980, NESSoS: Network of Excellence on Engineering Secure Future Internet Software Services and Systems.