We present a Petri net model of a protocol for the distributed generation of id-based private keys. Those keys can then be used for secure communications. The components of the system are built as refinements of a common interface, by applying a formal operation based on a class of morphisms between Elementary Net Systems. It is then shown that we can derive behavioural properties of the composed system without building it explicitly, by exploiting properties of the given morphisms.
In [
This framework was first defined relying on N-morphisms, originally
introduced in [
An α-morphism from an ENS N1 to an ENS N2 corresponds to a relation of refinement: some subnets of N1 refine conditions of N2. This refinement may require that some events be duplicated. Such morphisms are defined and discussed in Section 3.
When composing two ENS, N1 and N2 over an interface NI , the two morphisms towards the interface specify how each component refines parts of the interface. An uninterpreted example is given in Section 4.
One of the claimed advantages of this approach to design is the ability to derive properties of the composed systems from properties of the components and of the morphisms, without the need to actually build and analyse the composed system.
Ideally, one would like to derive behavioural properties, like liveness and safety properties, by analyzing only the structure of the models involved, thus avoiding the potentially high cost of computing the reachable markings. This is not always possible. Hence, the method we propose uses some behavioural information about components and interface; however, this is limited to only a part of the models, and does not involve the whole system model.
Here, we test these ideas on a protocol for distributed generation of id-based
cryptographic keys. The protocol, described in more detail in Section 5, requires
the cooperation of several private key generators (PKGs) so that a client can
build a private key. Basically, n PKG nodes come together to generate a master
key pair consisting of a private and a public key. After that, each PKG node has a
share for the master key pair. A client who wants to have a private key applies to
k available PKG nodes. Each PKG node calculates a piece of the client’s private
key by using the unique id-string of the client and the share of the master private
key which is held by that specific PKG node. On receiving k pieces, the client
continues to extract its private key. The so called bulletin board is responsible for
the initialization of the components in the system and broadcasting the public
parameters. During both the distributed generation of the master key pair and
the extraction of the clients’ private keys, a verification can be performed by
using the commitment values and public keys held and broadcast by the bulletin
board. The id-based distributed private key generation protocol was proposed
in [
In the next section, basic definitions related to ENS are recalled. Section 3 recalls the formal definition of α-morphisms and the properties they preserve or reflect and which are used in the rest of the paper. The definition of an operation of composition of ENS, based on α-morphisms, is informally recalled in Section 4 on the basis of an uninterpreted example. In the same section, the main result relating behavioral properties of the composed system to behavioral properties of its components is recalled. Section 5 presents the distributed private key generation protocol which is modelled by Petri nets in Section 6. In the same section, we analyze behavioural properties of the model. The paper is closed by a short concluding section. 2
In this section, we recall the basic definitions of net theory, in particular
Elementary Net Systems and unfoldings [
A net is a triple N = (B, E, F ), where B is a set of conditions or local states, E is a set of events or transitions such that B ∩E = ∅ and F ⊆ (B ×E)∪(E ×B) is the flow relation .
We adopt the usual graphical notation: conditions are represented by circles, events by boxes and the flow relation by arcs. The set of elements of a net will be denoted by X = B ∪ E.
The preset of an element x ∈ X is •x = {y ∈ X|(y, x) ∈ F }; the postset of x is x• = {y ∈ X|(x, y) ∈ F }; the neighbourhood of x is given by •x• = •x ∪ x•. These notations are extended to subsets of elements in the usual way.
For any net N we denote the in-elements of N by ◦N = {x ∈ X : •x = ∅} and the out-elements of N by N ◦ = {x ∈ X : x• = ∅}.
A net N 0 = (B0, E0, F 0) is a subnet of N = (B, E, F ) if B0 ⊆ B, E0 ⊆ E, and F 0 = F ∩ ((B0 × E0) ∪ (E0 × B0)). Given a subset of elements A ⊆ X, we say that N (A) is the subnet of N identified by A if N (A) = (B ∩ A, E ∩ A, F ∩ (A × A)). Given a subset of conditions A ⊆ B, we say that NA is the subnet of N generated by A if NA = (A, •A•, F ∩ ((A ∪ •A•) × (A ∪ •A•))). Note that given A ⊆ B, N (A ∪ •A•) = NA.
A State Machine is a connected net such that each event e has exactly one input condition and exactly one output condition: ∀e ∈ E, |•e| = |e•| = 1.
Elementary Net (EN) Systems are a basic system model in net theory. An Elementary Net System is a quadruple N = (B, E, F, m0), where (B, E, F ) is a net such that B and E are finite sets, self-loops are not allowed, isolated elements are not allowed, and the initial marking is m0 ⊆ B.
A subnet of an EN System N identified by a subset of conditions A and all its pre and post events, N (A ∪ •A•), is a Sequential Component of N if N (A ∪ •A•) is a State Machine and if it has only one token in the initial marking.
An EN System is covered by Sequential Components if every condition of the net belongs to at least a Sequential Component. In this case we say that the system is State Machine Decomposable (SMD).
Let N = (B, E, F, m0) be an EN System, e ∈ E and m ⊆ B. The event e is enabled at m, denoted m [ei, if •e ⊆ m and e• ∩ m = ∅; the occurrence of e at m leads from m to m0, denoted m [ei m0, iff m0 = (m \ •e) ∪ e•.
Let denote the empty word in E∗. The firing rule is extended to sequences of events by setting m [ i m and ∀e ∈ E, ∀w ∈ E∗, m [ewi m0 = m [ei m00[wim0; w is called firing sequence .
A subset m ⊆ B is a reachable marking of N if there exists a w ∈ E∗ such that m0 [wi m. The set of all reachable markings of N is denoted by [m0i.
An EN System is contact-free if ∀e ∈ E, ∀m ∈ [m0i: •e ⊆ m implies e• ∩ m =
∅. An EN System covered by Sequential Components is contact-free [
Let N = (B, E, F ) be a net, and let x, y ∈ X. We say that x and y are in conflict , denoted by x #N y, if there exist two distinct events ex, ey ∈ E such that exF ∗x, eyF ∗y, and •ex ∩ •ey 6= ∅, where F ∗ is the reflexive and transitive closure of F .
The semantics of an EN System can be given as its unfolding. The unfolding is an acyclic net, possibly infinite, which records the occurrences of its elements in all possible executions.
An occurrence net is a net N = (B, E, F ) such that if e1, e2 ∈ E, e1• ∩ e2• 6=
∅ then e1 = e2; F ∗ is a partial order; for any x ∈ X, {y : yF ∗x} is finite;
#N is irreflexive and the minimal elements with respect to F ∗ are conditions.
Occurrence nets were introduced in [
A branching process of N is an occurrence net whose elements can be mapped to the elements of N . Let N = (B, E, F, m0) be an EN System, and Σ = (P, T, G) be an occurrence net. Let π : P ∪ T → B ∪ E be a map. The pair (Σ, π) is a branching process of N if π(P ) ⊆ B, π(T ) ⊆ E; π restricted to the minimal elements of Σ is a bijection on m0; for each t ∈ T , π restricted to •t is injective and π restricted to t• is injective and for each t ∈ T , π(•t) = •(π(t)) and π(t•) = (π(t))•.
The unfolding of an EN System N , denoted by Unf (N ), is the maximal branching process of N , namely the unique, up to isomorphism, branching process such that any other branching process of N is isomorphic to a subnet of Unf (N ). The map associated to the unfolding will be denoted u and called folding. 3
α-morphisms
In this section we present the formal definition of α-morphisms [
We require that the map is total and surjective because N1 refines the abstract model N2, and any abstract element must be related to its refinement.
In particular, a subset of nodes can be mapped on a single condition b2 ∈ B2; in this case, we will call bubble the subnet identified by this subset, and denote it by N1(ϕ−1(b2)); if more than one element is mapped on b2, we will say that b2 is refined by ϕ.
In-conditions and out-conditions have different constraints, 5b and 5c
respectively. As required by 5c, choices which are internal to a bubble can not constrain
a final marking of that bubble: i.e., each out-condition of the bubble must have
the same choices of the condition it refines. Instead, pre-events do not need this
strict constraint (5b): hence it is sufficient that pre-events of any in-condition are
mapped on a subset of the pre-events of the condition it refines. Moreover, the
conditions that are internal to a bubble must have pre-events and post-events
which are all mapped to the refined condition b2, as required by 5d. By
requirement 5e, events in the neighbourhood of a bubble are not concurrent, and the
same holds for their images. Within a bubble, there can be concurrent events;
however, post events are in conflict, and firing one of them will empty the bubble
[
It is possible to show that the family of SMD-EN Systems together with
α-morphisms forms a category [
In [
Moreover, stronger properties hold under additional constraints. In order to present them, we have to consider the following construction. Given an αmorphism ϕ : N1 → N2, and a condition b2 ∈ B2 with its refinement, we define two new auxiliary SMD-EN Systems. The first one, denoted S1(b2), contains the following elements: a copy of the subnet which is the refinement of b2, i.e.: the bubble; its pre and post events in E1 and two new conditions, denoted bin and 1 bout. bi1n is pre of all the pre-events, and bout is post of all the post-events. The 1 1
bin initial marking of S1(b2) will be { 1 } or, if there are no pre-events, the initial marking of the bubble in N1. The second system, denoted S2(b2), contains b2, its pre- and post-events and two new conditions: bi2n, which is pre of all the pre-events, and bout, which is post of all the post-events. The initial marking of 2 S2(b2) will be {bi2n} or, if there are no pre-events, the initial marking of b2. Define ϕS as a map from S1(b2) to S2(b2), which restricts ϕ to the elements of S1(b2), and extends it with ϕS(bi1n) = bin and ϕS(bo1ut) = bo2ut. Note that S1(b2) and 2 S2(b2) are SMD-EN Systems and that ϕS is an α-morphism. Let Unf (S1(b2)) be the unfolding of S1(b2), with folding function u : Unf (S1(b2)) → S2(b2).
Consider the following additional constraints: c1 the initial marking of each bubble is at the start of the bubble itself; formally, for each b2 ∈ B2 one of the following conditions hold: – ϕ−1(b2) ∩ m10 = ∅ or – if •b2 6= ∅ then there is e1 ∈ ϕ−1(•b2) such that ϕ−1(b2) ∩ m01 = e1• or – if •b2 = ∅ then ϕ−1(b2) ∩ m10 = ◦ϕ−1(b2); c2 any condition is refined by a subnet such that, when a final marking is reached, this one enables events which correspond to the post-events of the refined condition, i.e.: ϕS ◦ u is an α-morphism from Unf (S1(b2)) (in which we put a token in the in-condition of the net) to S2(b2); c3 different bubbles do not “interfere” with each other; where we say that two bubbles interfere with each other when their images share, at least, a neighbour.
Note that the third constraint is not restrictive since the refinement of two interfering conditions can be done in two different steps.
Under c1, c2, and c3, the following properties can be proved [
for all m2 ∈ m20 , there is m1 ∈ m10 such that ϕ(m1) = m2; p2 N1 and N2 are weakly bisimilar: by using ϕ, define two labelling functions such that E2 are all observable, i.e.: l2 is the identity function, and the invisible events of N1 are the ones mapped to conditions; then (N1, l1) and (N2, l2) are weakly bisimilar (N1, l1) ≈ (N2, l2).
For a definition of weak bisimulation of EN Systems see [
In this section, we recall the composition of SMD-EN Systems based on
αmorphisms as defined in [
The two systems to be composed, N1 and N2, must be mapped onto a common interface, which is another SMD-EN System NI . The interface can be seen, intuitively, as a protocol of interaction, with which the components must comply, or as a common abstraction; in this second view, each component can refine some parts of the common abstraction. The two α-morphisms, from the components to the interface, determine how the two components refine the local states of the interface, and then which elements are to be identified and which events in the two components have to synchronize.
To compose two net systems, each must be canonical with respect to the corresponding morphism towards the interface. We say that a net system is canonical with respect to an α-morphism if each bubble contains a condition, called representation, that corresponds to the abstraction of that bubble. Examples of representations are rN1 (b1) and rN2 (b0) in Fig. 1. If a system is not canonical, it is always possible to construct its unique (up to isomorphism) canonical version by adding the missing representations, and marking them as their images, or by deleting the multiple ones. Because of the constraints on α-morphisms, and in particular of the ones on sequential components, point 5e of Def. 1, this construction does not modify the behaviour of the original system and the corresponding modified morphism is still an α-morphism.
In the example given in Figure 1 the interface NI is a simple sequence of two events. The two components, N1 and N2, refine two different local states, b1 and b0, each one by a subnet, shown on a gray background.
The composed net N = N1hNI iN2 contains the refinement of each condition
of the interface as it is in the two components, but for the representation, plus
the condition itself, as we can see for condition b0 and b1 of the example. The
rest of the net, not refined by the components, is taken as it is, but for the
synchronizations of the events in the neighbourhood of the refinements/bubbles.
Such events must be synchronized so that each possible pair composed by one
event of a component and one event of the other component must be created,
as we can see for events mapped on events e0 and e1 of Fig. 1. Then, also arcs
between in- and out-condition of each bubble and its pre and post (synchronized)
events must be created accordingly to the components. The initial marking is
the union of the ones in the components. By construction, N = N1hNI iN2 is an
EN System, and it is covered by sequential components [
This construction leads to the definition of a map ϕ0i from N = N1hNI iN2
onto Ni, i = 1, 2, relating each element local to a component to the corresponding
representation and projecting synchronized events. In [
ϕ2 ϕ01
ϕ02
N1hNI iN2 N1 d : N2
These results say that the composed system refines both the components,
as well as the interface. The main result relating behavioral properties of the
composed system to behavioral properties of its components is stated in the
following Proposition [
Proposition 1. Let Ni = (Bi, Ei, Fi, mi0) be an SMD-EN System for i = 1, 2, I. Let ϕi, with i = 1, 2, be an α-morphism from Ni to NI , and let N = N1hNI iN2 be be the composition of N1 and N2 using ϕ1 and ϕ2. If N1 is weakly bisimilar to NI then N = N1hNI iN2 is weakly bisimilar to N2.
Where, the labelling functions are derived from ϕ1 and ϕ02, respectively, in such a way that EI and E2 are all observable and the invisible events of E1 and E are the ones which are mapped to conditions by ϕ1 and ϕ02, respectively.
This result tells us, in particular, that the composition of refinements N1 and N2, which are weakly bisimilar to a common interface NI , yields a system N which is weakly bisimilar to NI ; and then, since bisimulation preserves deadlockfreeness, it is possible to deduce that N is also deadlock-free by verifying that NI is deadlock-free. Remember that by p2 it is possible to check weak bisimilarity between two systems related by an α-morphism by considering their behaviour only locally, as required by c1, c2, and c3. 5
In an id-based cryptographic system, unlike in the other public key cryptographic
systems, a publicly known string such as e-mail address, domain name, a physical
IP address or a combination of more than one strings is used as public key.
The idea of id-based cryptography was first proposed by Shamir in [
Basically, in an id- based cryptographic system there is a private key generator (PKG) which generates private keys for users. A PKG has a key pair which is referred as master key pair consisting of a master private key and a master public key. A PKG generates a private key for a user basically by first hashing its publicly known unique identity string then signing hashed id by the master private key. Later, the user can verify its key by using the master public key.
Since the PKG can generate private keys for users, it can sign or decrypt
a message for any user or it can make users’ private keys public. This problem
about private key generation is called the key escrow problem. Distributed
private key generation (DPKG) is one of the effective solutions to the key escrow
problem. In both schemes [
In a DPKG there is a number of PKG nodes participating while they share
the responsibility equally. In our work we followed the identity based distributed
private key generation schemes presented in [
The components of a DPKG system are divided into two main groups as PKG nodes and clients. PKG nodes are responsible for generating private keys for clients in a distributed manner. There is also a third component called bulletin board which is responsible for managing the global system variables, collecting the commitments from PKG nodes, calculating the final commitment and broadcasting these commitments.
We can examine DPKG protocol in three steps: setup, distribution and extraction. Setup is a preparation step to create the system parameters and to get ready for extracting the master key pair distributively and extraction of private keys. In this step, bulletin board is given a security parameter and chooses some system variables according to this given security parameter; it then broadcasts public system parameters to be used by the other system components. It also initializes the commitment values to zero in order to set them to the values it will receive from PKG nodes in the distribution step. Final commitment is also set to zero which will be calculated using the received commitments and it will be broadcast later.
Distribution step is illustrated in Figure 2. In this step, n PKG nodes create
a master private key together without using any dealer in a way that the key
cannot be reconstructed without retrieving k shares from these n PKGs. k is the
threshold number of PKG nodes needed to collaborate together in order to
construct the key. To do this, an improved version of (n, k) Feldman’s secret sharing
scheme stated in [
In extraction step, as it is illustrated in Figure 3, a client with identity string
ID contacts k available nodes from the PKG nodes pool. Each PKGi signs
hashed identity string of the client with its master private key share and returns
a private key piece as siH(ID) over a secure and authenticated channel. After
receiving k pieces from k available PKG nodes, client constructs its private key.
The client can verify the key by using bilinear pairings as it is stated in [
In this section, we present Petri net model of a simplified DPKG system with three PKG nodes while the threshold number is two. We fixed these numbers for the simplicity but the generated model is more generic and can easily be modified for different threshold and PKG node number as it will be discussed through this section. Our model consists of the following three nets: NI , NP KG and NC . NI is the common interface between NP KG and NC . It is an abstract model of the whole system which represents the interaction between the main components of the system. This model also includes the abstract behavior of the bulletin board which is basically responsible for managing the global system variables and commitments. NP KG is the net representing the behavior of PKG nodes while NC is the net representing the behavior of clients in the DPKG system. We aim to compose NP KG and NC using NI as the common interface and prove that the composed net NP KGhNI iNC and the interface NI preserve and reflect some properties presented in Section 3 since there is an α-morphism both from NP KG to NI and from NC to NI .
NI , which is the net representing the interface, is given in Figure 4. This net is an abstract model of the behavior of all three system components: bulletin board, PKG nodes and clients. The system is idle in the beginning. After event init occurs, system components are initialized and all PKG nodes are ready for generating a secret key distributedly. The event init includes the setup step of the protocol which is explained in Section 5. The condition calculate shares represents the whole process including calculating subshares and exchanging between PKG nodes in order to calculate their shares for the master private key. During this, each PKG node chooses a secret polynomial. It calculates the commitment corresponding to its secret polynomial and sends it to the bulleting board. It also calculates n subshares using its polynomial where n is the number of PKG nodes in the system. Each PKG node sends the subshare to the related PKG node. After exchanging is completed each PKG node will have n − 1 subshares sent by other PKG nodes and one subshare of its own. By using these n subshares each PKG node calculates its share. When the condition shares calculated becomes true, it means that all the PKG nodes finished calculating share and each of them is holding a share.
Once PKG nodes have their shares, they can verify their shares using the final commitment value which is already calculated during the abstract event calculate shares. If all the shares are correctly verified, the condition shares verified becomes true so a client can apply for extracting a private key. In this model, event apply includes choosing k available PKG nodes, receiving k pieces and calculating its private key using these pieces. When the condition key is true, the client has a key but we do not know if the key is correct or not by looking in this abstract model. In both cases new request event can occur or the system can continue with a restart which repeats the whole distributed private key generation. In case of a fail during the verification of shares, the system is forced to a restart without a key extraction.
NI is a live and reversible net which means that from any reachable marking one can always get back to the initial state. These two properties are important because a DPKG system must always be alive to respond to the clients’ key requests and key generation process must be restartable whenever it is needed. The net NI is also covered by sequential components which is a requirement in order to be able to look for an α-morphism. The sequential components covering the net can be shown as lists of conditions: {idle, ready, shares calculated, shares verified, key, restart requested }, {idle, client, key }.
Figure 5 shows the net NP KG. This net refines the interface with respect to PKG nodes’ behavior. All the elements of NP KG are mapped to the element with the same name in NI but for the subnet circled by dashed line that is
Fig. 5: NP KG, the net representing the PKG nodes. mapped to a single condition. This subnet forms a bubble which is a refinement of the condition shares calculated in NI . The bubble shows the calculation and exchange of subshares between three PKG nodes and calculation of shares by each PKG node whereas in NI the occurrence of the whole process is abstracted by one condition. If we model a system with n PKG nodes instead of three nodes, only the bubble will grow, the other elements of the net will remain the same.
NP KG is also live, reversible and covered by sequential components like NI . It is already shown that the conditions outside the bubble are covered by sequential components. Thus, here we will only show how the bubble is covered by sequential components. After event calculate shares the net branches into three paths and after each event calculate subshares i for i = 1, 2, 3 the net branches again into three paths. This fact results in having nine sequential components inside the bubble. Here we present only some of the sequential components as the lists of conditions that construct the components: {p1, subshare 1-2, subshare 1_2, share 2, shares calculated }, {p1, subshare 1-1, share 1, shares calculated }, {p1, subshare 1-3, subshare 1_3, share 3, shares calculated }. The paths starting with conditions p2 and p3 can also be constructed in the same way.
In order to prove that there is an α-morphism from NP KG to NI we have to show that the requirements in Definition 1 are satisfied. To begin with, the initial states of NP KG and NI are related. For all the events in NP KG which are mapped to an event in NI , also the pre-conditions and post conditions of these events are mapped to the pre and post-conditions of the related events in NI . Moreover, for all the events in NP KG that are mapped to a condition in NI , all the pre and post-conditions of that event are also mapped to the same condition in NI . We see that the nets satisfy the first four requirements of α-morphism. To continue with, we can see that the bubble in NP KG is acyclic so 5a is satisfied. As seen in Figure 5 all the in-elements of the bubble are generated by the only one event entering the bubble which is mapped to the corresponding event in the interface, calculate shares. It is also seen that post-events of the out-condition of the bubble are exactly the same post-events of the corresponding condition in the interface. Thus, 5b and 5c are satisfied. 5d is also satisfied because the conditions that are internal to the bubble have pre-events and post-events which are all mapped to the refined condition shares calculated in NI but for in and out-elements. Finally, as we already listed the sequential components of the net, it is easy to see that for each condition of the bubble there is a sequential component containing that condition and all the pre and post-events of the bubble, so requirement 5e is satisfied. In this way, we proved that there is an α-morphism from NP KG to NI .
The net shown in Figure 6, NC , is the net representing the behavior of a client. While it includes the whole abstract model, it refines the key extraction process of a client. The bubble shown with a dashed line is the refinement of the condition key in the interface NI . In this refinement, receiving two pieces from chosen PKG nodes, calculating the private key and verification of it is modeled in more details. In a DPKG system where the threshold number is two, when a client applies for a private key, it receives two pieces from two available PKG nodes. The client can verify the pieces it received. If both pieces are verified
Fig. 6: NC , the net representing the clients. then the client can extract its private key by using these pieces and the system reaches a state where extraction is successful. In case at least one of the pieces are not verified then the condition extraction not successful becomes true. After both failed or successful extraction, the system reaches a state where extraction ended is true and a new key can be requested by the same client or by any other client in the system. Again if we improve the model for threshold value k instead of two, only the bubble will grow but the other elements of the net will remain the same.
This net is also live, reversible and covered by sequential components. Here we give the sequential components which are enough to cover the net as lists of conditions: {idle, ready, shares calculated, shares verified, piece 1, piece 1 verified, piece 1 not verified, extraction successful, extraction not successful, extraction ended, restart requested }, {idle, ready, shares calculated, shares verified, piece 2, piece 2 verified, piece 2 not verified, extraction successful, extraction not successful, extraction ended, restart requested }, {client, idle, piece 1, piece 1 verified, piece 1 not verified, extraction successful, extraction not successful, extraction ended }.
It is very easy to see that the first four requirements of α-morphism are already satisfied so we can continue with checking the rest of the requirements. The bubble contains no cycles so 5a is satisfied. All the in-elements of the bubble are generated by the only one event entering the bubble which is mapped to the corresponding event in the interface, apply. There is also only one post-event of out-condition of the bubble which empties the bubble and this event is mapped to the post-event of key. With these observation it is easy to see that 5b and 5c are satisfied. 5d is also satisfied because the conditions that are internal to the bubble have pre-events and post-events which are all mapped to the refined condition key in NI but for in and out-elements.
Finally, as we already listed the sequential components of the net, it is easy to see that for each condition of the bubble there is a sequential component containing that condition and all the pre and post-events of the bubble, so requirement 5e is satisfied. Considering all the requirements, we can say that there is an αmorphism between NC and NI . Now that we proved that there is an α-morphism both from NP KG to NI and from NC and NI , we can prove that the composed net is weakly bisimilar to the interface by showing that some additional requirements which are stated as c1, c2, and c3 in Section 3 are satisfied by NP KG and NC . Proposition 1 states that if both of the components are weakly bisimilar to the interface, then the composed net is also weakly bisimilar to the interface. Thus, here we first show that NC is weakly bisimilar to the interface NI . To do this, we follow the construction of the two auxiliary nets given in Section 3, i.e., we consider the bubble in NC and the corresponding condition key in NI and we add their pre and post-events to the subnets. We also add two more conditions to each subnet: one condition to be a pre-condition to all pre-events and another condition to be a post-condition to all post-events. Let us name these two subnets as SC (key) and SI (key). Finally, we build the unfolding of SC (key), represented as Unf (SC (key)). The resulting nets are shown in Figure 7.
We follow the same procedure for NP KG and we get two subnets Unf (SP KG (shares calculated )) and SI (shares calculated) as in Figure 8.
When we examine these subnets, we see that no condition of the bubbles is in the initial marking. Any condition is refined by a subnet such that, when a final marking is reached, this one enables events which correspond to the post-events of the refined condition, so there is an α-morphism both from Unf (SC (key)) to SI (key) and from Unf (SP KG(shares calculated)) to SI (shares calculated). Thus, c1 and c2 are satisfied. Since there is only one bubble in both NP KG and NC , c3 is automatically satisfied. Consequently, we can say that the additional properties p1 and p2 are held. Moreover, considering Proposition 1, we can conclude that the composed net NP KGhNI iNC is weakly bisimilar to NI .
Knowing that our nets satisfy the requirements of α-morphisms and the other three additional constraints, give us the ensurance that, in addition to weakly bisimulation, the nets preserve another important property stated in p1. The property of reflecting reachable markings gives us a big advantage in performing reachability analysis. Instead of analyzing the big composed net with respect to reachability of a specific marking we can analyze the interface for the corresponding marking in the interface. To give an example, we can consider the existence of the following situation in the composed net NP KGhNI iNC : the condition shares verified should not be true while there is at least one token in any bubble. Performing a reachability analysis on the composed net is complex in terms of time and space since both the net and the logic formula we have to use to represent the interested global state are big. Instead, the mentioned global state can be easily translated into a global state of the interface, NI . Since each bubble in the composed net is mapped to a condition in the interface, reachability analysis becomes easier. The previously mentioned critical situation is reflected in the interface as the following: the condition shares verified cannot be true while key or shares calculated is true. Performing a reachability analysis for existence of this situation in NI is easier than analyzing the composed net. Moreover, we do not even need to build the composed net. 7
We have developed a Petri net model of a protocol for distributed generation of private keys. The model has been obtained by composing two net models on a common interface. The first component models the interactions among PKG nodes, while the second component models clients of the key generator. Both components refine a common interface, representing the interactions among components.
We have then discussed behavioural properties of the model, directly derivable from properties of the components without generating the composed net. In particular, we have shown that some markings are not reachable.
On one hand, we have verified modeling and analysis capacity of the
compositional approach proposed in [
We now plan to explore how to extend the approach to other classes of Petri nets, particularly PT nets and high-level nets. With respect to the model, we plan to improve it giving a less abstract specification in order to propose a formal verification of the protocol and to discuss its weak and strong aspects.
This work was partially supported by MIUR.