ABSTRACT

Group key security protocols play an important role in today’s communication systems. Their verification, however, remains a great challenge because of the dynamic characteristics of group key construction and distribution protocols. Security properties that are well defined in normal two-party protocols have different meanings and different interpretations in group key distribution protocols, specifically, secrecy properties, such as group secrecy, forward secrecy, backward secrecy, and key independence. In this paper, we present a method to verify forward secrecy properties for group-oriented protocols. The method is based on a correct semantical link between group key protocols and event-B models and also uses the refinement process in the B method to model and verify group and forward secrecy. We use an event-B first-order theorem proving system to provide invariant checking for these secrecy properties. We illustrate our approach on the Tree based Group Diffie-Hellman protocol as case study.

1. Introduction

Security protocols are used to establish secure channels between communicating systems. These protocols need great care in their development and their implementation. The complexity of security-protocol interactions can hide security weaknesses that normal analysis methods cannot reveal. Security properties that are well defined in normal two-party protocols have different meanings and different interpretations in group key distribution protocols. Therefore, they require a more precise definition before we look at how to verify them. For group key distribution protocols, secrecy property has a further dimension since there are long term secret keys, short-term secret keys, in addition to present, future, and past keys; where a principal who just joined the group and learned the present key should not be able to have enough information to deduce any previous keys, or similarly a principal who just left the group should not have enough information to deduce any future keys.

In group key protocols, there are generally four types of security properties [1]: group key secrecy, which guarantees that it is computationally infeasible for a passive adversary to discover any group key, intuitively, that the attacker should not be able to obtain a key that honest users think to be safe; forward secrecy, which guarantees that a passive adversary who knows a contiguous subset of old group keys cannot discover any subsequent group key; backward secrecy, which guarantees that a passive adversary who knows a contiguous subset group keys cannot discover preceding group keys, and finally, key independence, which guarantees that a passive adversary who knows a proper subset of group keys cannot discover any other group key.

Event-B [2] was introduced by extending B [3] without changing it to model operations that could be guarded in the process algebraic sense. The event-B method uses the set-theoretical and logical notations of the B method and provides new notations for expressing abstract models based on events. It provides invariants proofs based on a state-based system that is updated by guarded events. The refinement capability offered by event-B allows incremental development moving from an abstract level to a more concrete one. Refinement technique allows the preservation of proved properties and therefore it is not necessary to prove them again in the refined transition system. Moreover, in the refinement, it is not needed to re-prove these properties again while the model complexity increases. This advantage is important compared to classical model checking where the transition system describing the model is refined and enriched.

Group key protocols have special features, such as the concept of group secrecy, forward secrecy, and dynamic group events. These feature were rarely considered or addressed thoroughly when formal verification techniques were applied. In this paper, we provide an event-B based invariant checking for verification of group key protocols. We model group key protocols and verify their required properties, in particular secrecy and forward secrecy properties, using the event-B method. Event-B deals with tools allowing invariant checking, and can be used to verify group key secrecy properties. In order to model a group key protocol in event-B first order logic, a formal relation between the semantics of the event-B language [4] and the protocol model should be defined. This mapping relation should present the semantics of group key protocol model based on event-B, hence, allowing the verification of secrecy properties. This allows us to avoid user interaction with the theorem proving tool, and reduce the time required to verify these properties. This paper extends the work in [5] to verify forward secrecy using event-B refinement.

We apply our approach on the tree based Group Diffie-Hellman (TGDH) protocol [6] and provide invariant checking for secrecy under the static and the dynamic case by applying a single event (join/leave). We use the event-B first order prover platform Rodin [7,8] to perform invariant checking under the assumption that basic Diffie-Hellman key is correct. The dynamic case is also considered by applying events such as join and leave and verify the correctness of key construction for bounded tree size and bounded number of events. We assume perfect cryptography conditions in our approach. In addition the group key protocol is analyzed in the presence of passive adversaries.

The rest of the paper is organized as follows. Section 2 discusses related work to ours. In Section 3, we present our methodology to verify forward secrecy using event-B refinement. In Section 4, we apply our approach on TGDH protocol. Finally, Section 5 concludes the paper with future work hints.

2. Related Work

The recent years have seen the emergence of successful applications of formal approaches to reasoning about security protocols. Earlier methods were concerned with reasoning about the events that a security protocol can perform, and make use of a causal dependency that exists between protocol events. Methods like strand spaces [9] and the inductive method of Paulson [10] have been designed to support an intensional, event-based, style of reasoning. These methods have successfully tackled a number of protocols though in an ad hoc fashion. They make an informal spring from a protocol to its representation and do not address how to build up protocol representations in a compositional fashion [11].

Events-based verification of security protocols was used by Crazzolara [11] using mappings between process algebra, Petri nets, strand spaces and inductive models. The authors established precise relationships between the Petri nets semantics and transition semantics, strand spaces, inductive rules, trace languages, and event structures. They show how event-based models can be structured in a compositional way and so used to give a formal semantics to security protocols which support proofs of the correctness of these protocols. They demonstrated the usefulness of their Petri nets semantics in deriving proof principles for security protocols and apply them to prove an authentication property.

Cremers [12] proposed an operational semantic for security protocols. The work provides a generic description of the interpretation of such security protocols and what it means for a protocol to ensure some security property. This work imposes explicit static requirements for valid protocols, and verifies that the model is parametric with respect to the matching function and intruder network capabilities. Other related work that treats group key protocols verification, specifically DH based protocols, are discussed in more details in [13].

Stouls and Potet [14] proposed a method to automatically enforce an abstract security policy on a network. They used the B refinement process to build a formal link between concrete and abstract terms, which is dynamically computed from the environment data. The method is applied on a case study modeling a network monitor. A different approach to achieve a similar objecttive was proposed in [15], where the authors addressed the proof-based development of system models satisfying a security policy. They used OrBAC [16] models to express the security policies in order to state permissions and prohibitions on actions. An abstract B model is derived from the OrBAC specification of the security policy and then the model is refined to introduce properties that can be expressed in OrBAC. The refinement guarantees that the resulting B model satisfies the security policy.

Bert et al. [17] presented a tool to build symbolic labeled transition systems from B specifications. The resulting symbolic transition system represents all the behaviors of the initial B event system. The tool, called GeneSyst, was illustrated on a security property for a model of a smart card purchase transaction protocol. Butler [18] combined CSP and B method refinement in order to verify authentication property. The work does not present a new theoretical framework, instead it describes the use of the above methods to treat refinement of secure communication systems.

Chridi et al. [19] presented a decision procedure for the sub-class of Well-Tagged protocols with Autonomous Keys to analyzing Web Services manipulating sequences of items. Dalal et al. [20] provided a comparative and evaluation study for tools used in verification of security protocols. In another related work, Li [21] and Pand extended the strand space method to include time and timstamps to model the notion of recency in Kerberos protocol.

Compared to the above, we address security properties for group oriented protocols, which have special features that were not addressed in any of these approaches, such as the concept of group secrecy and forward secrecy and dynamic group events. In addition, we consider events that are specific for group key protocols that were never treated by the Event-B method. In [13], we used the rank function based inference system to model and verify two parties Diffie-Hellman protocol, while in [5], we presented an approach for modeling and verification of group key protocols by using event-B first-order logic invariant checking. The method is based on a formal link between the semantics of group key protocols model and event-B based on a well-formed connection between event-B invariant and the group key protocol model including its secrecy property. This paper extends the work in [5] to verify forward secrecy property using event-B refinement. We define two models for the group protocol: an abstract model and a refined model. The first one captures secrecy property as an invariant for the abstract model, and the second one captures forward secrecy as an invariant for the refined model.

Many methods were developed to verify certain aspects of security protocols such as secrecy and authenticcation. These methods have successfully tackled a number of protocols though in an ad hoc fashion. On the other hand, using formal methods like model checking can be efficient in the verification of authentication property, while modeling and reasoning about properties like forward secrecy requires first-order-logic based methods such as Event-B.

3. Event-B Method

Event-B [2] is a variant of the B method introduced by Abrial [3] to deal with reactive systems. An event consists of a guard and an action. The guard is a predicate built on state variables and the action is a generalized substitution which defines a state transition. An event may be activated once its guard evaluates to true and a single event may be evaluated at once. The system is assumed to be closed and it means that every possible change over state variables is defined by transitions; transitions correspond to events defined in the model. The B method is based on the concept of machines [3]. A machine is composed of descriptive and operational specifications:

A descriptive specification describes what the system does by using a set of variables, constants, properties over constants and invariants which specify properties that the machine’s state verify. This constitutes the static definition of the model. Operational specification describes the way the system operates. It is composed of a set of atomic events described by generalized substitutions. An event has a guard and an action, and it may occur only when its guard evaluates to true. An event has one of the general forms where the SELECT form is just a particular case of the ANY form. SELECT takes the

form

 Name event =

  ANY P WHERE

   G

  THEN R

and similarly a SELECT statement takes the form

nbsp;Name event =

  WHEN

   G

  THEN

   R

3.1. Event-B Invariant Checking

The consistency of an event-B model is established by proof obligations which guarantee that the initialization verifies the invariant and that each event should preserve the invariant. The guard and the action of an event define a before-after predicate for this event. It describes a relation between variables before the event holds and after this. Proof obligations are produced from events in order to state that the invariant condition is preserved. Let M be an event-B model with v being variables, carrier sets or constants. The properties of constants are denoted by, which are predicates over constants, and the invariant by. Let E be an event of M with guard and before-after predicate that indeed yields at least one after value. The initialization event is a generalized substitution of the form. Initial proof obligation guarantees that the initialization of the machine must satisfy its invariant:.

Each event E, if it holds, has to preserve the invariant. The feasibility statement is illustrated in Lemma 3.1 and the invariant preservation is given in Lemma 3.2 [4].

Lemma 3.1..

Lemma 3.2..

An event-B model M with invariant I is well-formed, dented by, only if M satisfies all proof obligetions. The B syntax for generalized substitutions defines three predicates: a relation R, the subsets of the pre-states where G is true of the states in, and the subset of the pre-state where P is true. Let S be restricted to evaluations that satisfy the invariant,. Each event can be represented by a binary relation rel formally defined as. The fact that the invariant is preserved by event rel is simply formalized by saying that rel is a binary relation built on S:. It is shown that this binary relation yields to both Lemmas 3.1 and 3.2 above [4].

Lemma 3.1 guarantees that the active part of the relation is a total relation, i.e., when all predicates I, P, and G hold, formally, , while Lemma 3.2 guarantees that the postcondition of any operation must satisfy the machine invariant. The initial proof obligation guarantees that the initialization of a machine must satisfy its invariant.

We distinguish special rules for the initialization events. We use to denote the predicate of the generalized substitution associated with this event. Then we obtain the following initialization statements [4]:

Lemma 3.3.

Lemma 3.4.

3.2. Event-B Refinement

Refinement is a technique to deal with the development of complex systems. It consists in building, starting from an abstract model, a sequence of models of increasing complexity containing more and more details. These details could be introduced when using new variables, adding details to abstract events or adding new events. A model in the sequence is followed by a model it refines. The invariant of the refined model is not weaker than the model it refines and it may contain new variables. The events are the same but may be redefined. It is also used to transform an abstract model into a more concrete version by modifying the state description [22]. The abstract state variables, v, and the concrete ones, , are linked together by means of a gluing invariant. A number of proof obligations ensures that 1) each abstract event is correctly refined by its corresponding concrete version; 2) each new event refines skip; 3) no new event takes control forever; and 4) relative deadlock fairness is preserved. Suppose that an abstract model A_M with variables v and invariant is refined by a concrete model C_M with variables vc and gluing invariant. If and are, respectively, the abstract and concrete before-after predicates of the same event, we have to prove the following statement:

This statement means that under the abstract invariant and the gluing invariant, a concrete step can be simulated by an abstract one in such a way that the gluing invariant is preserved. A new event with before-after predicate must refine skip. This leads to the following statement to prove:

.

Moreover, we must prove that a variant (valuation of variable v) is decreased by each new event (this is to guarantee that an abstract step may occur). We have thus to prove the following for each new event with before-after predicate:

.

At last, we must prove that a concrete model does not introduce more deadlocks than the abstract one. This is formalized by means of the following proof obligation:

where stands for the disjunction of the guards of the events of the abstract model, and stands for the disjunction of the guards of the events of the concrete one. The essence of the refinement relationship is that it preserves already proved system properties including safety properties. The invariant of an abstract model plays a central role for deriving safety properties; the goal is to obtain a formal statement of properties through the final invariant of the last refined abstract model.

4. Event-B Semantics Based Verification Methodology

In order to reason about group protocols in the first-order logics, a map between the group protocol model and event-B model semantics is defined. The event-B tool guarantees the correctness of the invariant w.r.t the event-B model. The map from group protocols to eventB model guarantees certain equivalence between the two models, under certain conditions. Secrecy property is semantically implied in event-B invariant in a defined and proved lemma. Then, a theorem is defined to guarantees that once an event-B invariant is proved against event-B mode, we can conclude that the secrecy property is correct for the group protocol mode.

In the event-B method, compared to higher-order logic, the number of protocol participants that can be considered is limited, finally, modeling forward and backward simultaneously requires more than two levels of abstracttion, hence, generates more proof obligations, which will reduce automation as more interaction with the tool will be required to discharge these obligations, this is an open issue to be addressed in future work. Figure 1 depicts the formal links in the proposed event-B approach.

The security property is defined in the event-B model based on mapping sets, events, and invariants. For forward secrecy, we use refinement of secrecy. The soundness of the event-B model is then established based on a well-formed link to the group protocol model. The validity of the event-B invariant against its model is checked using the Rodin invariant checking tool. This way, we establish the formal link from the Rodin langauge to the group protocol model.

Let be a group key protocol model, and let be a set of all possible messages (messages space). We choose to represent the secret messages space, the set of all secret messages,. Thereafter, we define to be the set of all events, or dynamic operations, i.e., join, leave, merge, and split. An event is a term from the message space to the message space,. It represents an action the user can perform on the system to update his/her own set of knowledge.

Let be the set of initial knowledge of the intruder, where. The initial knowledge of the information is collected before executing the protocol events. This information is usually publicly known, . We then define as the set of knowledge of the intruder that is updated by executing events. The system starts with the initial set of knowledge and the set of events, then, by executing a sequence of events, it updates this set. and.

We define a safety property for a group key protocol model. This property states that the system cannot execute an event in in order to generate a message in, and is formally modeled as follows:

.

If this property is correct for the protocol, then we can write.

Forward secrecy guarantees that a passive adversary who knows a contiguous subset of old group keys (say) cannot discover any subsequent group key for all i and j, where. We will follow this definition in our model for the rest of the paper.

The proposed verification methodology consists of a number of steps as shown in Figure 2. In the first step, the group key protocol is specified formally using the model presented before in order to obtain precise proto-

col specifications. In addition, the secrecy property expected to be checked by the system is described informally. In the second step, the obtained specification is translated into event-B specification using mapping relations to obtain an event-B model that captures the features of the group protocol model. Next, a secrecy property is specified as an invariant of the resulting event-B model I, and a forward secrecy property is specified as an invariant of the refined event-B model. Messages can be defined as a set with an enumeration of all possible secret and known messages. The intruder initial knowledge, , is directly defined as variable or set in the event-B initialization list. Secret messages are defined similarly. Protocol initial constraints, such as and, are defined as properties that will be included in the invariant. Protocol join or leave events are defined as event-B operations that update the intruder’s knowledge and the set of secret messages, including the new generated key. Finally, the property is checked from the obtained global system specification using the event-B invariant checking in Rodin platform.

In Figure 3, protocol events and execution traces are mapped into event-B events, messages generation conditions are mapped into events guards, and messages sets are used to generate event-B model constants properties. The initial knowledge is defined as event-B initializetions, messages are mapped directly into sets, and finally the secrecy property is defined as an invariant for the event-B model. The generation of the target event-B model requires treating three parts: the static part which includes initializations and the constant properties of the protocol, the dynamic part that represents events of the protocol, and finally, enriching the resulting model with invariants describing the required secrecy properties.

The event-B semantics is close to the protocol model semantics. This relationship is demonstrated by establishing a well-formed link between the semantics of both models. To achieve this link, we are interested in showing that if the invariant I holds for event-B system M, then the safety property must hold for the group protocol model. Formally,. In terms of equivalence between the two models, we can say that the event-B model M is an abstract model of the protocol model, with regards to the security property, if the property holds in the model, and the invariant I holds in the abstract model M. To illustrate this equivalence, we need to show that. Therefore, it is

enough to show that the invariant I, with regards to M, implies the safety property, with regard to.

4.1. Verification of Secrecy as Event-B Invariant

To show that, we need to establish a well-formed link between event-B invariant and the safety property. We split this formal link into two parts: the first deals with the initialization, and the second deals with executing the events. For this, we need to relate messages in to variables in M by mapping public messages and secret messages to event-B sets and messages sets to event-B constants properties. This map relates the variable m over the set of messages directly to the variable v over event-B carrier sets and constants. The semantical correspondence between the variable m and the variable v is defined by this map.

Theorem 4.1. Secrecy Soundness.

A group protocol, G, satisfies its secrecy property, , if there is an equivalent abstract event-B model, M, that satisfies an event-B invariant, I, and implies the property. More formally, for a model G, we need to find an abstract model M where means that the event-B model M can be abstracted from the group protocol G. This abstraction will be defined later. Let, and be correct lemmas, then,

.

The proof is divided into two parts, in the first we assume that holds, then we prove the theorem based on that. In the next stage we prove each lemma separately and we identify the relation between G and M such that holds.

Proof. Given, , and, we can deduce

We establish the abstract relation between G and M such that holds, then we prove the lemma. The lemma is assumed to be correct in the event-B tool.

Definition 4.1. A group protocol model G, is abstracted to an event-B model, M under certain conditions and semantically correct map from G to M. is defined as follows:

For every component and condition in G there is an equivalent one in M. A protocol model is composed of, we map each component in G into an equivalent one in M.

Messages sets are mapped into an event-B variable by defining v over the set, and messages sets relations are mapped to event-B constants properties. is a function of. These relations include the predicates about sets that should always hold.

Messages generation conditions are mapped into events guards. These conditions include predicates that should hold prior to executing an event, like having the appropriate key to encrypt or decrypt a message.

The secrecy property, , is mapped into an event-B invariant, I. This map is defined in Lemma 4.1.

An event in is mapped into event R, an event, with a precondition condition, where , the message generated from executing the even, can be defined concretely using an event-B statement such as:

Name event =

ANY mWHERE condition THEN

This map defines the relation.

To show that, we need to establish a wellformed link between event-B invariant and the safety property. We split this formal link into two parts: the first deals with the initialization, and the second deals with executing the events. First we relate messages in to variables in M. In Figure 3, we describe a map from public messages and secret messages to event-B sets and a map from messages sets relations to event-B constants properties. This map relates the variable m over the set of messages directly to the variable v over event-B carrier sets and constants. The semantical corresponddence between the variable m and the variable v is defined by this map.

We define the invariant I as, where is the invariant predicate under the initial conditions, and is the invariant predicate under executed events. Similarly, we define the safety property.

Lemma 4.1.

Proof. We define the well-formed conditions that guarantee the correctness of this lemma in two steps, we first show that. We identify the initial events and initial set of messages in under which the formula holds. Then we define the predicates P, I, G, and R presented in Lemmas 3.1 and 3.2 for the protocol model such that Lemma 4.1 holds.

The definition of the group key protocol must satisfy the initial soundness conditions: and , where is an initial event that can be applied on the intruder's initial set of messages. We choose to be the set of events that can be executed on.

We will define the constants property P and the initialization predicate for the model that will satisfy Lemmas 3.3 and 3.4. Then we define P, R, the predicate guards G, and the invariant I for the model that will satisfy Lemmas 3.1 and 3.2.

Case 1.

•

•

The message generation event is equivalent to the transition relation. This yields the formula which is exactly Lemma 3.3 considering that.

The invariant definition for the model is . We need to show that the invariant I holds for both and. Since the protocol is initially sound, then both and hold by the fact that and that the initial events cannot generate secret messages in S. If then. Therefore we can write , which corresponds to Lemma 3.3 considering that.

Case 2.

•

•

•

This message generation event is equivalent to the transition relation. Therefore, applying the predicates P, I, and G will lead to the relation R. We can write the formula which is equivalent to Lemma 3.1 considering that the relation R is equivalent to an existing event.

The validity of the invariant for the model is expressed by the validity of the predicates P, I, R, and G, where. This can be written as , which corresponds to Lemma 3.2.

Under these conditions, we guarantee that when the invariant holds in event-B model, the secrecy property definition holds for the group key protocol model. These predicates should be considered carefully when providing the event-B implementation. Properties that can be expressed as invariants are verified using the translation process and the event-B tool.

This completes the proof of Theorem 4.1. The major restriction on this method is that it can reason about the execution of a single protocol event, i.e., join or leave. However, this is enough to model and verify group secrecy when a member joins or leaves the group.

4.2. Verification of Forward Secrecy Using Event-B Refinement

Figure 4 illustrates the modifications required on the verification methodology in order to support forward secrecy. When the invariant I holds for event-B system M, the safety property must also hold for the group protocol model. The verification methodology for forward secrecy is built on top of the methodology we use for secrecy. In order to apply invariant checking on forward secrecy, we will consider the model M as an abstract one, and define a refined model, , and a gluing invariant J linking variables of the abstract model to those of the concrete or refined one (). In addition to the previous map defined from G to M, we will use the variable to represent the set of intruders messages in the refined model. Therefore, will represent the gluing invariant which represents forward secrecy property before the relation. In addition, we use to represent the invariant in the refined model, which corresponds to the secrecy property of the refined protocol model,. The relation will be defined the same way as the relation R.

In event-B, refinement can be done with events or variables. In our case, the group protocol join or leave events have the same semantics in both secrecy and forward secrecy, therefore, it will have the same definition in both the abstract and refined event-B models, i.e.,. We use to represent join or leave events, which update the intruder’s set of knowledge, the variable v here. In the refined model, we will use the same relation, we call it, that will update the intruder’s set of knowledge, , in the refined model.

The correctness of forward secrecy, , with regards to the event-B concrete model is achieved through the correctness of the gluing invariant. Figure 5 below illustrates the link between the abstract and refined model to achieve a model for forward secrecy in event-B.

A group protocol, , satisfies its secrecy property, , if there is an equivalent event-B model, M, that satisfies an event-B invariant, I, and a refined event-B model that satisfies an event-B invariant I, and a gluing variable that implies in the existence of a relation.

Formally, given, , , and, then

.

Assuming, , and, we can deduce:

.

.

This way, we guarantee that once a refined event-B

model is verified against its invariant, then the group protocol model is verified against its forward secrecy property.

Event-B invariant checking cannot reason about backward secrecy because invariants cannot be used in a reverse manner, i.e., refining the intruder’s knowledge back in time. In backward secrecy the intruder is assumed to be an active user in the group while trying to discover older secret shares prior to his/her membership. Therefore, refinement of secrecy can only be used for forward secrecy. Based on this, key independence (collusion) cannot also be modeled in this method as is.

5. Case Study: The TGDH Protocol

In this section, we apply the approach on a group key protocol that generates a key in a distrusted group. We show how the conditions defined for the correctness of the above model can be concretely applied on a real protocol. The intended secrecy property, along with its conditions, are efficiently defined and checked as event-B invariant.

The Tree-based Group Diffie-Hellman protocol (TGDH) is intended for secure key generation. Figure 6 shows a binary tree structure that represents the group members, their own secret shares, and the secret sub-keys on every node up to the root. As part of the protocol, a group member can take on a special sponsor role, which involves computing intermediate keys and broadcasting to the group. Each broadcasted message contains the senders view of the key tree, which contains each blind key known to the sender [1].

A group key can be computed from any members secret share and all blind keys on the co-path to the root. Blind keys are the siblings of the nodes on the key path. The members own secret share and all sibling blind keys on the path to the root enable a member to compute all intermediate keys on its key-path, including the root group key.

The group key is calculated by each member based on his/her key-path and blind keys. For instance, for a member M₃ at node, the key-path is the set of messages. The set of blind keys ordered as they appear up to the root is

. The group key at the root is calculated directly using the two sets:

The protocol designers presented four types of security properties: group key secrecy, forward secrecy, backward secrecy, and key independence. The authors of [1] provided an informal proof that their protocol satisfies these security property. In this work, we provide a formal proof for group key secrecy property under certain conditions. This property can be described as a correct key construction property, which guarantees that only group members, who are of knowledge to their own private shares, can calculate the group key at root. On the other hand, an adversary, who knows all blind sub-keys cannot find a full path to calculate the root key.

We illustrate our method on a group protocol composed of three members, then we apply a join event for a fourth member. Figure 7 shows the modification on the tree structure when a new member joins the group, we define the group protocol components before and after this event takes place. Assuming that a passive adversary is monitoring the group activity, the knowledge set is built based on the blind keys interchanged between members. Based on this, we show all group protocol components, including secrecy property, and the equivalent event-B model including the invariant, before the

join event takes place:

where the sets of messages, , , and.

Then, we show the same components after the join event of a new member with a new secret contribution. Note that group key secrecy has the same definition and should be valid always, before and after a join (or leave) event takes place.

5.1. Secrecy Model in Event-B Invariant

The event-B model for the protocol components is described below. We describe the current status of the group by initializations appropriate sets for messages and keys. The secrecy property is defined as an invariant that combines a set of conditions to be satisfied at the initialization and after executing the event:. Some of the protocol characteristics can also be encoded within this invariant, such as. We also define an event to represent the protocol action (join/ leave).

The TGDH protocol components are defined within the event-B model. The group key has basically the same definition, and secrecy property is defined as an event-B invariant that contains, in addition to group key secrecy, certain conditions on messages sets to ensure the consistency of the map,

.

An event-B definition that captures the behavioral semantics of a join event which will result in updating the intruder’s set of knowledge is described as follows:

MACHINE  M0 SEES  P0     

VARIABLES K  GKey  S pwn INVARIANTS inv1: K Key GKey Key S M inv2: pwn N × N K inv3: K ∩ S = GKey K EVENTS Initialisation begin

act1: M := {n₁, n₂, n₃, pwn(g, n₁), pwn(g, n₂), pwn(g, n₃), pwn(g, n₁ * n₂), pwn(g, n₂ * n₃), pwn(g, pwn(n₁ * n₂)), pwn(g, n₃ * g(n₁, n₂))}

act2: K := {n_i, pwn(g, n_i), pwn(g, n₁), pwn(g, n₂), pwn(g, n₃), pwn(g, pwn(g, n₁ * n₂))}

act2: Key := {pwn(g, n₃ * pwn(g, n₁ * n₂))}

act3: S := {n₁, n₂, n₃, pwn(g, n₁ * n₂), pwn(g, n₃ * pwn(g, (n₁ * n₂)))}

act4: GKey := {pwn(g, n₃ * pwn(g, n₁ * n₂))}

end Event  join any n₄

where grd1: n₄ M then

act5: M := M {n₄, pwn(g, n₄), pwn(g, n₃ * n₄), pwn(g, pwn(g, n₃ * n₄) * pwn(g, (n₁ * n₂)))}

act6: S := S {n₄, pwn(g, n₃ * n₄), pwn(g, pwn(g, n₃ * n₄) * pwn(g, (n₁ * n₂)))}

act7: GKey := pwn(g, pwn(g, n₃ * n₄) * pwn(g, (n₁ * n₂)))

act8: Key := Key {GKey}

act8: K := K {n₄, pwn(g, pwn(g, n₃ * n₄))}

Event  IntEvnt any m1, m2 where grd1: m1 K m2 K then act1: K := K {pwn(m1, m2)}

END The intruder set of knowledge is modeled with K in the above model, and is initialized with the public set of knowledge. We assume the intruder has access to the knowledge of users leaving the group. Therefore, with the execution of each event, this knowledge is updated dynamically. The function pwn models the exponent operator used to calculate keys. After the join event is executed, the new key will be generated and added to that set of secret keys based on the contribution of the joined member, n₄, as follows:

For the verification of the invariants, we first consider the static case of key construction under the assumption that basic DH key construction (on tree leaf nodes) is correct. We then consider the dynamic case by applying events such as join and leave and verify the correctness of key construction for a bounded tree size and bounded number of events. The event-B invariant has been proven totally. The number of generated proof obligations are three, all proof obligations are discharged, and then the initial model of the group key protocol is validated. The event-B invariant, I, defined in the Rodin platform above, implies the group protocol secrecy semantically,. The event-B tool guarantees that. We have shown in the previous section that the group protocol G is mapped into an event-B model M. Therefore, we can conclude the correctness of the secrecy property for the protocol model G,.

The proposed solution allows us to verify the required property, however, one limitation of our approach is its applicability on bounded number of participants and protocol events, this issue will be addressed in the future work. Another limitation is due to the fact that we verify the property under the execution of a single event. However, this approach is sufficient for the target property, where key distribution is abstracted away because we are concerned only with modeling key construction but not key distribution or authentication property. Even though there are some limitations for the approach, event-B can be used in modeling specific protocols behaviors, like key construction, and tree-based protocol primitives can be modeled directly in event-B for safety properties verification.

5.2. Forward Secrecy Model with Event-B Refinement

We illustrate the method on a group protocol composed of four members, then we apply a leave event for a specific member. Figure 8 shows the modification on the tree structure when a new member leaves the group, we define the group protocol components before and after this event takes place. This represents the abstract model. When a new member joins the group, the knowledge set is built based on the blind keys interchanged between group members and the observing member’s old set of knowledge who left the group earlier (Figure 8). This represents the refined model.

In Figure 8(a), the current set of messages, secret set of messages, and the current group key are defined, respectively, as follows:

Then, after member M₄ joins the group, as shown in Figure 8(b), the above variables become:

The next step, is that we let member, who will be assumed to be dishonest later, leave the group, where a new secret share is generated as in Figure 8(c). The above variables become:

Finally, Figure 8(d) is the join (or similarly leave) event on which we will check invariant for the refined model. The event represents the join event for the new member. is a dishonest user who will take advantage of this event. We first illustrate secrecy, then forward secrecy:

The intruder knowledge, K, as viewed by a member monitoring the group from outside, before joins the group is defined as:

Then we show the set of messages when member joins the group:

Secrecy implies that the intruder monitoring the group should not be able to calculate the group key GroupKey_d (or any secret share or sub-key).

In forward secrecy, the set of messages K is refined with the knowledge gained by user while member in the group, and is denoted:

Group key protocol secrecy properties were defined as invariants in Rodin platform, the tool generates proof obligations that were successfully discharged using event-B proof control. The results achieved here are important because our method allows semi-automated verification of these properties under dynamic operation of the protocol. In addition, the method allows modeling protocols at different levels of abstraction, where the model can be further refined in order to include more details about the protocol operation.

6. Conclusions

In this paper, we provided invariant checking approach for group key secrecy and forward secrecy. We used event-B invariants to model and verify group key secrecy, then, on top of this, we used event-B refinement to model and verify forward secrecy. For this purpose, a formal link between the semantics of the group protocol model and event-B was established. The result was combining the event-B and group protocol model to be able to use specific features in event-B to model protocol actions and verify the required property. However, we restrict the group protocol model to be verified to certain conditions in order to guarantee the correctness of the method and the applicability of first-order logic theorem proving. This includes the number of participants, abstracting the exponentiation operator for Diffie-Hellman style protocols, and finally, applying a single protocol event.

We applied this approach on a group key protocol, the tree based Group Diffie-Hellman protocol and provided invariant checking for secrecy under the static and the dynamic case by applying a single event (join/leave). In contrast to our work, the authors of this protocol [1] provided an informal, non-intuitive and simple proof for secrecy property.

Even though our approach can model and verify only invariant properties, while liveness related properties cannot be modeled in our approach, we believe that invariant checking is adequate to model secrecy related properties. This is due to the target model and the verifycation tool, namely, event-B and Rodin platform. EventB supports only safety related properties which are modeled and verified as invariants. In addition, a limited class of liveness properties can be modeled using invariants, such as termination, while more general liveness properties are not supported yet in Event-B. Hoang and Abrial [23] have an ongoing research for reasoning about liveness properties in Event-B.

As future work, an interesting issue to be considered is modeling and verifying liveness security properties using event-B. In addition, an extension of the event-B based model to handle a parameterized number of participants shall be explored. It will also be interesting to investigate modeling backward secrecy and key independence using event-B.

REFERENCES