Keywords

1 Introduction

Security protocols are notoriously known to be difficult to get right. Designing error-free security protocols that are impervious to attack techniques, such as freshness and interleaving sessions (i.e. impersonation attacks, man-in-the-middle attacks, oracle attacks, multiplicity attacks and other types of parallel session attacks) is an extremely challenging task [1, 2]. Many protocols proposed in the literature and many protocols exploited in practice turned out to be flawed, or their well-functioning was found to be based on implicit assumptions. Such as the Needham-Schroeder authentication protocol, initiated a large body of work on the design and analysis of cryptographic protocols. In 1995, Gavin Lowe published an attack on the protocol that had apparently been undiscovered for the previous 17 years [3].

However, for security protocols, most of them are designed to meet specific application environment according to actual needs based on the intuition and experience of researchers. It turns out that designing security protocols based on experience and other informal methods has security vulnerabilities.

Formal methods have the characteristics of concise analysis process, and is recognized as an effective way to analyze the security of network protocols [4, 5]. For this reason, researchers have been working on the use of formal verification techniques to analyze the vulnerability of security protocols. A large number of formal methods have been proposed, which including modal logic, theorem proving and model checking [6,7,8].

In 2005, a framework (denoted DDMP framework) consisting of Protocol Derivation System (PDS) and Protocol Composition Logic (PCL) [9, 10] has been proposed by Datta et al. PDS supports syntactic derivations of complex protocols, starting from basic components, and combining or extending them using a sequence of composition, refinement, and transformation operations [11]. PCL is a Floyd-Hoare style logic that supports axiomatic proofs of protocol properties. The eventual goal is to develop proof methods for PCL for every derivation operation in PDS, thereby enabling the parallel development of protocols and their security proofs. Since the DDMP framework was proposed, this method has been successfully applied to the formal analysis and security proof of many protocols. Datta et al. described the deduction process of various protocols in STS family, and successfully analyzed ISO-9798-3. Roy et al. [12] extended the original PCL for the confidentiality of security protocol. Mitchell et al. [13] have successfully analyzed industrial protocols such as SSL/TLS and Kerberos V5 using PCL. Li et al. [14] proposed a PCL secure user authentication protocol named UCAP for cloud computing. Zhang Junwei et al. [15] proposed a PCL secure and efficient group authentication protocol named TSNP. PCL is an effective way to provide formal proofs to the correctness of security protocols.

There is no doubt that DDMP framework has been successfully applied to a number of industrial network security protocols. However, there are only a little improvement on the PCL rather than PDS after the DDMP framework.

PDS for deriving security protocols consists of a set of basic building blocks named components and a set of operations for constructing new protocols from old ones. These operations can be divided into three different types: composition, refinement and transformation. A component is used as a building block for larger protocols. For example, the Diffie-Hellman key exchange and challenge-response component are basic components providing the desired security properties. The composition operation combines two sub-protocols. Parallel composition and sequential composition are two composition operations. The refinement operation acts on message components of a single protocol. The original PDS mainly aims at the design of two-party interaction protocols including initiator and responder, without the existence of a Trusted Third Party. In addition, the main set of operations for PDS is public key encryption [16]. Although Zhang Junwei et al. [17,18,19] added some new components, refinements and transformation to the PDS, their work mainly aims to derive the key exchange protocols in the Needham-Schroeder family. Therefore, in order to derive key agreement protocols using a Trusted Third Party in symmetric encryption environment, we intend to extend the PDS.

Our Contributions.

In this paper, we study the extension of PDS to support the derivation of key agreement protocols using a Trusted Third Party in symmetric encryption environment.

  1. 1.

    Some components, refinements, transformations and removing redundancy rules are added to the PDS. The extended PDS can carry out protocol design using combination method based on symmetric encryption environment.

  2. 2.

    A flow chart of deriving security protocols based on the extended PDS is given. The flow chart consists of two layers, the first layer is to get a raw protocol using components, refinements, transformations, the second layer is to remove superfluous protocol steps and improve protocol efficiency.

  3. 3.

    Deriving a key agreement protocol in symmetric environment is given as an example to illustrate how the extended PDS supports the derivation of security protocols.

The rest of this paper is organized as follows. Section 2 introduces some preliminaries about PDS and the defects of PDS. Section 3 gives the extension of PDS. In Sect. 4, we give the detailed derivation of security protocols to illustrate how to derive protocols based on the extended PDS. Section 5 concludes.

2 Protocol Derivation System and Its Defects

PDS is a useful method to design and generate security protocols syntactically, which consists of a set of basic building blocks called components and a set of operations for constructing new protocols from old ones. First, we give brief introduction about components, operations and transformations, then the defects in PDS are presented.

2.1 The Explanation of Symbols

A, B, S: :

Initiator, Responder and Server (Trusted Thirty Party).

K: :

shared key. In symmetric encryption environment, the encryption key is the same as the decryption key, which can be written as K = K−1.

Na, Nb::

random numbers generated by A and B.

m: :

A message.

Kxy::

the shared key Kxy between X and Y.

SIG X (m): :

A signature of m created by X.

X → Y: :

X sends a message m to Y.

p ⇒ q::

block p is replaced by block q

2.2 Components

A protocol component consists of a set of roles (e.g., initiator, responder, server), where each role has a sequence of inputs, outputs and protocol actions. Diffie-Hellman key exchange and signature-based authenticator are basic components in PDS.

Diffie-Hellman Component, C1

The Diffie-Hellman protocol [20] provides a way for two parties to set up a shared key (gir) which a passive attacker cannot recover. There is no authentication guarantee: the secret is shared between two parties, but neither can be sure of the identity of the other. The initiator and responder role actions are given below.

I::

generates random value i and computes gi (for previously agreed base b)

R::

generates random value r and computes gr (for previously agreed base b)

In this component no messages are sent.

Signature-Based Authenticator, C2

The signature-based challenge-response protocol shown below is a standard mechanism for one-way authentication.

I → R::

m

R → I::

SIGr (m)

It is assumed that m is a fresh value or nonce and that the initiator, I, possesses the public key certificate of responder, R, and can therefore verify the signature.

2.3 Composition

The composition operation used is sequential composition of two protocol components with term substitution. The roles of the composed protocol have the following structure: the input sequence is the same as that of the first component and the output is the same as that of the second component; the actions are obtained by concatenating the actions of the first component with those of the second (sequential composition) with an appropriate term substitution-the outputs of the first component are substituted for the inputs of the second.

2.4 Refinements

  • Refinement R1 SIGX (m) ⇒ EK (SIGX (m)), where K is a key shared with the peer. The purpose of this refinement is to provide identity protection against passive attackers

  • Refinement R2 SIG X (m) ⇒ SIG X (HMACK (mIDX)), where K is a key shared with the peer. While the signature by itself proves that this term was generated by X, the keyed hash in addition proves that X possesses the key K.

  • Refinement R3 SIGX (m) ⇒ SIGX (m), HMACK (m, IDX), where K is a key shared with the peer. This refinement serves the same purpose as R2.

  • Refinement R4 SIGX (m) ⇒ SIGX (mIDY), where Y is the peer. It is assumed that X possesses the requisite identifying information for Y, e.g., Y’s public key certificate, before the protocol is executed. This assumption can be discharged if X receives Y’s identity in an earlier message of the protocol.

  • Refinement R5 gx ⇒ gx, nx, where nx is a fresh value. The use of nonce enables the reuse of exponentials across multiple sessions resulting in a more efficient protocol.

  • Refinement R6 SIGX (m) ⇒ SIGX (m), IDX, where IDX denotes the public key certificate of X. This refinement enables that the principals possess each other’s public key certificates before the session.

  • Refinement R7 EK (m) ⇒ EK (m), HMAC K’ (role, EK (m)), where K and K’ are keys shared with the peer and role identifies the protocol role in which this term was produced (initiator or responder).

2.5 Transformations

Message Component Move, T1

This transformation moves a top-level field t of a message m to an earlier message m’, where m and m’ have the same sender and receiver, and if t does not contain any data freshly generated or received between the two messages. One reason for using this transformation is to reduce the total number of messages in the protocol.

Binding, T2

Binding transformations generally add information from one part of a protocol to another in order to “bind” the two parts in some meaningful way. The specific instance of this general concept that we use here adds a nonce from an earlier message into the signed portion of a later message, this operation is illustrated as follows.

figure a

Cookie, T3

The purpose of the cookie transformation is to make a protocol resistant to blind Denial-of-Service (DoS) attacks [21]. Under certain assumptions, it guarantees that the responder does not have to create state or perform expensive computation before a round-trip communication is established with the initiator.

figure b

To sum up, key agreement protocols using a Trusted Thirty Party differ from the STS family and Needham-Schroeder family in the following characteristics.

  1. 1.

    Involvement of a Trusted Third Party. There are only the Diffie-Hellman component and signature-based authenticator component in PDS, which can’t derive key agreement protocols using a Trusted Thirty Party

  2. 2.

    Symmetric encryption. Due to the lack of components and operations to describe this kind of encryption type in PDS, symmetric key exchange protocol can’t be derived by PDS.

  3. 3.

    More interactive steps. Because of the involvement of Trusted Third Party and symmetric encryption-based authentication, it’s necessary to remove superfluous protocol steps and improve protocol efficiency by removing redundancy rules.

3 The Extension for PDS

For the original PDS exists some defects, an extended PDS is proposed. Not only some components and transformations are added in the extended PDS, but also some removing redundancy rules which don’t exist in original PDS are proposed, the purpose of these rules is to reduce superfluous protocol steps and improve efficiency.

3.1 Extended Components

Timestamp Component, C3

A → S: :

{A, B}K as

S → A: :

(A, M, T S )K as , (B, M, T S )K bs

The client requests from the server. If the request information is encrypted and intercepted by a third party to the request package, the request package can be used for repeated requests. If the server does not prevent replay attack, the server pressure will increase, and the use of timestamp can solve this problem.

Trusted Thirty Party Component, C4

A → S: :

A, B

S → A: :

K ab

A → B: :

K ab

This component is a basic framework for key agreement protocols with Trusted Thirty Party. In this component, the initiator A sends his identity and B’s identity to the server. Then the server responds with shared key Kab between A and B. Finally, the initiator sends Kab to B. This component can provide key agreement but don’t ensure authentication and confidentiality.

Challenge-Response Component, C5

C → R: :

N C

R → C: :

E K {m, N C }

In contrast to signature-based authenticator component C2, this component is encrypted by symmetric key and the request information is a random number rather than message m. Using a series of Challenge-Response steps, which can provide user authentication to some degree.

Three-Party Authentication Component, C6

A → B::

A, {A, N a } K as

B → S::

{N b , B}K bs , {A, N a } K as

S → B::

{Na, N b }K bs

The three-party authentication component C6 is a basic framework for key agreement protocols using a Trusted Third Party. Because of the existence of Na and Nb, This Component can ensure the authentication between A and B through a Trusted Thirty Party.

3.2 Extended Refinements

Refinements are mainly for the cryptographic operation of messages in the protocol. Without changing the number of messages or the structure of the protocol, the necessary security attributes can be added to a message component by refinements.

There are seven refinements R1–R7 in the existing PDS system, which are mainly for public key cryptosystem. The cryptographic refinement operations based on symmetric key encryption are as follows.

  • Refinement R8: m → EK (m). The message m is encrypted by symmetric key K, no one can decrypt message EK (m) unless the agent discloses its own private key. This refinement can guarantee the confidentiality of message m to some degree.

  • Refinement R9: EK(m) → EK(m, X). The identity of X is added to EK (m), therefore this refinement can prevent man-in-middle attack effectively.

  • Refinement R10: EK{Na} → EK(Na−1). Responding the message EK(Na−1) rather than EK{Na}, which can refresh the random number Na and prevent reply attack effectively.

  • Refinement R11: EK(X) → EK(X, Na). By adding the random number Na, this refinement can prevent reply attack to some degree because of the freshness of Na

3.3 Extended Transformations

Symmetry, T8

figure c

Changing Order, T9

figure d

Index, T10

To denote a run of protocol, we add a unique index to every step of transformed protocol.

figure e

Consistency, T11

Sometimes we need to ensure the consistency of shared key through key agreement protocols, so the transformation T11 is proposed.

figure f

3.4 Removing Redundancy Rules

There are some redundant operations and items in redundancy protocol, which leads to redundant authentication and affects efficiency. At the same time, the operation items in the security protocol are too long, which will affect the efficiency, especially when both agents use public key to achieve security properties. Therefore, we introduce the following removing redundancy rules.

Cascade Connection, RR1

If there are multiple encryption structures in the protocol step i, and these encryption structures use the same cryptographic algorithm and key, thus these can be combined into one structure. The cascade connection is expressed in logical language as follows:

figure g

Deleting Duplicate Information, RR2

If the same message appears twice in a protocol step, only one of them is retained. The deleting duplicate information is expressed in logical language as follows:

figure h

Freshness, RR3

If the data items used to prove freshness in protocol step i (such as random numbers) always appear at the same time as a data item with freshness in the protocol, then the data items used to prove freshness can be deleted. The rule is expressed in logical language as follows:

figure i

Plaintext, RR4

If a plaintext m appears in the encryption part of the protocol, the plaintext m is encrypted first and then simplified by cascade connection RR1.

4 Deriving Security Protocols Based on the Extended PDS

Based on the extended PDS, we give a flow chart to derive security protocols. This flow chart can be divided into two layers. The first layer is to get a raw protocol meeting expected security properties. First, combining the basic cryptographic primitives, we can get some components, which are the basic framework for different kinds of security protocols. According to expected security properties, for example, the mutual authentication or the key agreement between initiator and responder, choosing some correct components and then getting a single step protocol. Next, based on the composition rules, appropriate refinements and transformations, a raw protocol can be concluded. The second layer is to remove redundancy and improve efficiency. Through removing redundancy rules, a target protocol can be derived. The above steps are illustrated in Fig. 1.

Fig. 1.
figure 1

The flow chart of deriving security protocols based on the extended PDS

Full size image

In order to better illustrate how to derive a security protocol based on the extended PDS, we will derive a three-party key agreement protocol as a case study.

  1. 1.

    First, our objective protocol is a three-party key agreement protocol, so we choose C4 as the basic component, which provides key agreement using a Trusted Thirty Party.

  2. 2.

    Protocol P1 obtained by applying R8 to C4.

    A → S::

    A, B

    S → A::

    {Kab}Kas, {Kab}Kbs

    A → B::

    {Kab}Kbs

  3. 3.

    Protocol P2 obtained by applying T9 to P1.

    A → B::

    A

    B → S::

    A, B

    S → B::

    {Kab}Kas, {Kab}Kbs

    B → A::

    {Kab}Kas

  4. 4.

    Protocol P3 obtained by applying T10 to P2.

    A → B::

    M, A

    B → S::

    M, A, B

    S → B::

    M, {Kab}Kas, {Kab}Kbs

    B → A::

    M, {Kab}Kas

  5. 5.

    The goal of key agreement can be achieved by protocol P3 basically. Now we need to add component C6 which provides mutual authentication between initiator and responder. Protocol P4 obtained by applying C6 to P3.

    A → B::

    M, A, {Na, A}Kas

    B → S::

    M, A, B, {Na, A}Kas, {Nb, B}Kbs

    S → B::

    M, {Kab}Kas, {Na, A}Kas, {Kab}Kbs, {Nb, B}Kbs

    B → A::

    M, {Kab}Kas, {Na, A}Kas

  6. 6.

    We can learn that some messages are encrypted by the shared key, It’s necessary to remove superfluous protocol steps and improve protocol efficiency. So protocol P5 obtained by applying cascade connection RD1 to P4.

    A → B::

    M, A, {Na, A}Kas

    B → S::

    M, A, B, {Na, A}Kas, {Nb, B}Kbs

    S → B::

    M, {Kab, Na, A}Kas, {Kab, Nb, B}Kbs

    B → A::

    M, {Kab, Na, A}Kas

  7. 7.

    Protocol P6 obtained by composition P5 and T8.

    A → B::

    M, A, B, {Na, M, A, B}Kas

    B → S::

    M, A, B, {Na, M, A, B}Kas, {M, Nb, A, B}Kbs

    S → B::

    M, {Kab, Na, Nb, A}Kas, {Kab, Nb, B}Kbs

    B → A::

    M, {Kab, Na, Nb, A}Kas

  8. 8.

    Protocol P7 obtained by applying T11 to P6.

    A → B::

    M, A, B, {Na, M, A, B}Kas

    B → S::

    M, A, B, {Na, M, A, B}Kas, {M, Nb, A, B}Kbs

    S → B::

    M, {Kab, Na, Nb, A}Kas, {Kab, Nb, B}Kbs

    B → A::

    M, {Kab, Na, Nb, A}Kas, {Nb}Kab

These above steps are shown in a flow chart Fig. 2.

Fig. 2.
figure 2

Deriving three-party key agreement protocol based on the extended PDS

Full size image

The final protocol P7 is an AOR protocol, whose security properties have been proved by PCL in reference [22].

Through the combinations and refinements of the basic components, the target security protocol is obtained. Compared with a security protocol based on expert intuition and experience, the target security protocol obtained in this paper is more secure to a certain extent. Of course, to further ensure the security properties the target protocol, we can provide logical proof for the security protocols based on PCL.

In additional, in order to illustrate the advantage of the extended PDS, we give an overall comparison with Datta [9] and Zhang Junwei’s methods [17, 18].

 

Trusted Third Party

Symmetric Encryption

Removing Redundancy Rules

Timestamp

Three-Party Authentication

Datta

\( \times \)

\( \times \)

\( \times \)

\( \times \)

\( \times \)

Zhang Junwei

√

√

\( \times \)

\( \surd \)

\( \times \)

This paper

√

√

√

√

√

Compared with Datta and Zhang Junwei’s methods, the main advantages of this paper add a Trusted Third Party, removing redundancy rules and three-party authentication component, which support the derivation of public key or symmetric key protocols with trusted third party. In addition, some removing redundancy rules are added in the PDS in order to reduce redundant information and improve efficiency.

5 Conclusions

PDS is a useful method to design and generate security protocols syntactically. However, the PDS is only applicable for two-party interaction protocols, which does not involve in the presence of a Trusted Third Party. In this paper, we proposed an extended PDS that can support key agreement protocols using a Trusted Thirty Party by adding some components, refinements, transformations and removing redundancy rules. A flow chart of deriving security protocols based on the extended PDS is given. The flow chart consists of two layers, the first layer is to get a raw protocol using components, refinements, transformations, the second layer is to remove superfluous protocol steps and improve protocol efficiency by removing redundancy rules. We get the improved version of Otway-Rees protocol as an example to illustrate how to derive a security protocol based on the extended PDS.

In DDMP framework designed by Datta, PCL can provide logical proof for the security protocols generated by PDS. But at present, PCL can’t support the logical proof of every step in the PDS system. In additional, deriving different types of security protocols supported by PDS is still our future work.