In a distributed system, in which an action can be either “hidden” or “observable”, an unwanted information flow might arise when occurrences of observable actions give information about occurrences of hidden actions. A collection of relations, i.e. reveals and its variants, is used to model such information lfow among transitions of a Petri net. This paper introduces a parametrised generalisation to the existing reveals relations and provides a formal basis for information-flow analysis of bounded equal-conflict PT systems.
In distributed systems, it is often the case that some actions are confidential, and it is not desired that a user is able to deduce information about occurrences of these confidential actions, while still being able to interact with the system. This kind of unwanted information flow can form a security concern for systems. Noninterference is a formal notion which guarantees that a system does not sufer from such information flow.
The concept of noninterference was introduced by Goguen and Meseguer for deterministic
state machines in [
Busi and Gorrieri moved the notion of noninterference to 1-safe Petri nets by studying
observational equivalences and structural properties in [
The work presented in [
In [
In this paper, we extend the results in [
The paper is organised as follows. Section 2 provides the necessary background on Petri nets. Section 3 recalls some definitions of reveals relation in the context of information flow and introduces new parametric variants. Section 4 formalises maximal-step computation tree and its full prefix for bounded equal-conflict PT systems and provides methods for computing reveals relations for positive information-flow analysis on full prefix. Section 5 concludes the paper and discusses some possible future work.
In this section we recall basic definitions concerning Petri nets and net unfoldings that will be
useful in the rest of the paper, see also [
A net is a triple = (, , ), where and are disjoint sets. The elements of are called places and are represented by circles, the elements of are called transitions and are represented by squares, ⊆ ( × ) ∪ ( × ) is the flow relation , represented by directed arcs. The pre-set of an element ∈ ∪ is the set ∙ = { ∈ ∪ : (, ) ∈ }; the post-set of is the set ∙ = { ∈ ∪ : (, ) ∈ }. Let ⊆ ∪ be a subset of elements, its pre-set is defined as ∙ = { ∈ ∪ : ∃ ∈ : (, ) ∈ }, and its post-set as ∙ = { ∈ ∪ : ∃ ∈ : (, ) ∈ }.
A net (, , ) is a subnet of another net ( ′, ′, ′) if ⊆ ′, ⊆ ′ and is the restriction of ′ to ( × ) ∪ ( × ).
A net is finite if ∪ is finite, and infinite otherwise. A net is T-restricted if for any ∈ , ∙ ̸= ∅ and ∙ ̸= ∅.
A Place Transition (PT) system, Σ = (, , , , 0) is defined by a finite net (, , ), a map : → N which assigns a positive weight to each arc, and an initial marking 0 : → N. We write (, ) = 0 when (, ) ∈/ . The tuple (, , , ) will be called PT net. In graphical representations, arcs are inscribed by their weights, if the weight is greater than one, and markings are represented by () dots, called tokens, in each place .
Let Σ be a PT net and : → N be a marking. A transition is enabled at , denoted [⟩, if, for any ∈ , () ≥ (, ). Let be enabled at ; then, can occur (or fire ) in producing the new marking ′, denoted [⟩′ and defined as follows: ∀ ∈ , ′() = () − (, ) + (, ).
A finite or infinite sequence of transitions 12 ... ... is an occurrence sequence enabled at 0, denoted 0[1 ... ... ⟩, if there are intermediate markings 1 ... ... such that: 0[1⟩1 ... [⟩ ....
Let be a marking of Σ, the set [⟩ is the smallest set of markings such that: ∈ [⟩, and if ′ ∈ [⟩ and ′[⟩′′, then ′′ ∈ [⟩. The set [0⟩ is the set of reachable markings of Σ.
A multiset of transitions : → N is concurrently enabled at ∈ [0⟩, denoted [ ⟩, and called step, if ∀ ∈ , ∑︀∈ () · (, ) ≤ (); if is enabled at , it can occur producing the new marking ′, denoted [ ⟩′ and defined as follows: ∀ ∈ , ′() = () − ∑︀∈ () · (, ) + ∑︀∈ () · (, ).
A multiset : → N is a maximal-step at ∈ [0⟩ if [ ⟩ and ∀′ ∈ , ∃ ∈ such that: () < ∑︀∈ () · (, ) + (, ′).
Analogously to occurrence sequences, a finite or infinite sequence of steps (or maximalsteps) 12...... is a step sequence (or a maximal-step sequence) enabled at 0, denoted 0[1......⟩, if there are intermediate markings 1...... such that: 0[1⟩1...[⟩....
Two transitions 1 and 2 are in conflict at a marking ∈ [0⟩ if they are both enabled at , [1⟩ and [2⟩, however they are not concurrently enabled at , ¬([{1, 2}⟩), the occurrence of one of them disables the other one.
In some situations concurrency and conflicts overlap in such a way that it is not clear if in
the execution of concurrent transitions a conflict has been solved or not. This is a so called
situation of ‘confusion’ which has been introduced by C.A. Petri and discussed in several papers
as for example in [
The relation between step semantics and maximal-step semantics has been studied for example
in [
A general class of nets in which confusion cannot arise is the class of equal-conflict PT nets,
studied by various authors, see for example [
From the definition, it follows that in EC PT systems, if two transitions share a pre-place, then any given marking enables either both transitions or neither. All the figures in this paper, except for Fig. 1, provide examples of EC PT systems.
A PT system Σ is bounded if there is a finite number such that: for any reachable marking ∈ [0⟩ and for any place , () ≤ . If Σ is bounded, its set of reachable markings [0⟩ is finite. A marking is a deadlock if no transition is enabled in . Σ is 1-live if for all ∈ there exists ∈ [0⟩ such that [⟩.
In the rest of the paper, we will consider finite, bounded, and 1-live PT systems, whose underlying nets are T-restricted.
We now introduce two technical relations that will be useful to define the partial order semantics of PT systems. The ≺ relation on the elements of a net is the transitive closure of and ⪯ is the reflexive closure of ≺ . Let , ∈ ∪ , #, if there exist 1, 2 ∈ : 1 ̸= 2, 1 ⪯ , 2 ⪯ and there exists ∈ ∙ 1 ∩ ∙ 2.
A net = (, , ), possibly infinite, is an occurrence net if the following restrictions hold: 1. ∀ ∈ ∪ : ¬( ≺ ) 2. ∀ ∈ ∪ : ¬(#) 3. ∀ ∈ : { ∈ ∪ | ⪯ } is finite 4. ∀ ∈ : |∙ | ≤ 1 In an occurrence net, the elements of are called conditions and the elements of are called events; the transitive and reflexive closure of , ⪯ , forms a partial order. The set of minimal elements of an occurrence net with respect to ⪯ will be denoted by min( ). Since we only consider T-restricted nets the elements of min( ) are conditions.
A configuration of an occurrence net = (, , ) is a, possibly infinite, set of events ⊆ which is causally closed (for every ∈ , ′ ⪯ ⇒ ′ ∈ ) and free of conflicts (∀1, 2 ∈ , ¬(1#2)). is maximal if it is maximal with respect to set inclusion.
On the elements of an occurrence net the relation of concurrency, co, is defined as follows: let , ∈ ∪ , co , if neither ( ≺ ) nor ( ≺ ) nor (#).
A B-cut of is a maximal set of pairwise concurrent elements of , and can be intuitively seen as a global state of the net in a certain moment. An E-cut of is a maximal set of pairwise concurrent elements of , that corresponds to a maximal step on .
A branching process of a bounded 1-live PT system Σ = (, , , , 0), whose underlying net is T-restricted, is a pair (, ), where = (, , ′) is an occurrence net, and is a map from ∪ to ∪ such that: 1. () ⊆ ; () ⊆ 2. ∀ ∈ , ∀ ∈ , (, ()) = | − 1() ∩ ∙ | and ( (), ) = | − 1() ∩ ∙ | 3. ∀ ∈ 0() = | − 1() ∩ min()| 4. ∀, ∈ , if ∙ = ∙ and () = (), then =
We extend the definition of to the set of configurations of the branching process: for each configuration , () is the multiset of the transitions whose occurrences are recorded in and is called the footprint of ; formally () = ∑︀∈ (). If a transition belongs to the support set of (), i.e.: at least an occurrence of is in , ()() ≥ 1, then we use the notation ∈ (). If is infinite, it records the infinite occurrence of some transitions, and the multiset () is such that the multiplicity of those transitions is infinite, whereas its support set is obviously finite, being a subset of .
A branching process (1, 1) is a prefix of a branching process (2, 2) if 1 is a subnet of 2 containing all minimal elements (min(2)) and such that: if ∈ 1 and (, ) ∈ 2 or (, ) ∈ 2 then ∈ 1; if ∈ 1 and (, ) ∈ 2 then ∈ 1; and 1 is the restriction of 2 to 1 ∪ 1.
Any finite PT system Σ = (, , , , 0) has a unique branching process which is maximal with respect to the prefix relation. This maximal branching process, called the unfolding of Σ, will be denoted by Unf(Σ) = ((, , ′), ), where is the map from (, , ′) to (, , ).
A run records a possible non sequential behaviour of the system, it is a branching process, whose occurrence net is free of conflicts, i.e., its set of events is a configuration. A run is maximal if the corresponding configuration is maximal. Let be a run, its footprint ( ) is equal to the footprint of its set of events.
Example 1. Figure 2 represents an equal-conflict PT system Σ and a branching process, which is a prefix of the unfolding of Σ. A maximal run of the branching process is the labelled subnet whose elements are grey, the set of its events is the configuration = {1, 2, 3, 4, 5, 6}, The footprint of is the multiset () = {, , , , 2.ℎ}.
In [
Let Σ = (, , , , 0) be a PT system (bounded, 1-live PT system with T-restricted underlying net) and Unf(Σ) = ((, , ), ) be its unfolding. In the following, will denote the set of all maximal configurations of Unf(Σ). The set of events of Unf(Σ) corresponding to a specific transition of a given PT system Σ will be denoted by = { ∈ : () = }. We will assume progress of the system, i.e., an enabled transition either fires or gets disabled by another transition in conflict with it; the set of configurations satisfying this assumption coincides with .
The reveals relation was originally introduced for events of an occurrence net in [
Definition 1. Let 1, 2 ∈ be two transitions; 1 reveals 2, denoted 1 ▷ 2, if 1 ∈ () =⇒ 2 ∈ (). ∀ ∈
Since we consider 1-live nets, there is at least one maximal configuration in which 1 occurs. If there exists a maximal configuration in which 1 occurs and 2 does not occur, then 1 ̸▷ 2.
Sometimes, even if a transition alone does not give much information about the occurrence of
another transition, a set of transitions together might imply the occurrence of some transitions
in another set. This relation was originally defined for the events of an occurrence net in
[
Note that _ is not defined if the transitions of never appear together. Remark 1. Extended reveals relation between two singletons coincides with reveals relation.
The next relation takes the repeated occurrences of a transition into account. In some cases,
the occurrence of a transition does not give information while several occurrences of the
transition imply the occurrence of another transition. This relation was defined in [
Definition 3. Let 1, 2 ∈ be two transitions, and be the set of all maximal configurations of Unf(Σ). Let be a positive integer. If there exists a maximal configuration in which 1 occurs at least times, then we say 1 -repeated reveals 2, denoted .1 ▷ 2, if
∀ ∈ | ∩ 1 | ≥ =⇒ ∩ 2 ̸= ∅.
Note that -repeated reveals is not defined if there is no maximal configuration in which occurs at least times.
The following statements are direct consequences of Def. 3. 1
Remark 3. If .1 ▷ 2 and ∃ ∈ such that | ∩ 1 | ≥ + 1 then ( + 1).1 ▷ 2. Remark 4. .1 ̸▷ 2 =⇒ ( − 1).1 ̸▷ 2.
Example 2. A bounded equal-conflict PT system is illustrated in Fig. 3. In this system, the occurrence of implies the occurrence of since every maximal configuration which has also has . However, vice versa is not correct since there is a maximal configuration in which occurs without . Thus, ▷ and ̸▷ . Some other reveals relations are ▷ , ▷ , ▷ ℎ, ℎ ▷ , ▷ and ℎ ▷ .
Examples of extended reveals are as follows. The occurrence of alone or alone is not suficient to say something about the occurrence of , but the occurrence of and together implies the occurrence of , i.e., {, } _ {}. Although ̸▷ and ̸▷ , the occurrence of implies the occurrence of either or , i.e., {} _ {, }. Similarly, {} _ {, }.
Examples of repeated reveals are as follows. Only one occurrence of does not give information about , but if occurs twice, this implies the occurrence of , i.e., 2. ▷ . Similarly, two occurrences of imply the occurrence of ℎ, i.e., 2. ▷ ℎ.
The following variant of reveals relation is parametric and it generalises all the variants above. This relation is more expressive and allows one to specify the expected security requirements in a more tailored fashion.
Definition 4. Let , ≥ 1 and {1, ..., } be positive integers. Let {1, ..., }, ⊆ . If there is at least one maximal configuration in which each transition of {1, ..., } occurs at least times, then we say {1.1, ..., .} extended-repeated reveals denoted {1.1, ..., .} _ if ∀ ∈
⋀︁ ∈{1,...,} (| ∩ | ≥ ) =⇒
Note that {1.1, ..., .} extended-repeated reveals is not defined if there is no maximal configuration in which each transition of {1, ..., } occurs at least times. Remark 5. Reveals, extended reveals and repeated reveals can be expressed by Def. 4.
1 ▷ 2 ⇐⇒ {1.1} _ {2}, {1, 2} _ {3, 4} ⇐⇒ {1.1, 1.2} _ {3, 4},
.1 ▷ 2 ⇐⇒ {.1} _ {2}.
Example 3. In the system net illustrated in Fig. 3, let us examine the relation between the transitions , and . Neither nor reveals alone. There is no extended reveals or repeated reveals relation between them either. However, there is still some information flow. Two occurrences of together with two occurrences of extended-repeated reveal , i.e., {2., 2.} _ {}. This might cause a security violation in a system where the occurrence of is supposed to be a secret.
Let us consider a case in which the total number of occurrences of a set of transitions gives information about another set of transitions. In other words, if the total number of occurrences of the transitions in the first set is more than a certain number, this implies that at least one transition of the second set must have occurred or will occur inevitably. The next relation defines such situation. If a set of low transitions collectively reveal some high transitions this might cause a security violation.
Definition 5. Let ≥ 1 and , ⊆ . If there is at least one maximal configuration in which the total number of occurrences of the transitions in set is at least , then we say -collective reveals , denoted . _ , if ∀ ∈ ∑︁ | ∩ | ≥ =⇒ ∈
Note that -collective reveals is not defined if there is no maximal configuration in which the total number of occurrences of the transitions in set is at least .
1 ▷ 2 ⇐⇒ 1.{1} _ {2}, .1 ▷ 2 ⇐⇒ .{1} _ {2}.
Example 4. In the net in Fig. 4, if the total number of occurrences of and is at least 3, this implies the occurrence of ℎ, i.e., 3.{, } _ {ℎ}.
In the net in Fig. 5, if the total number of occurrences of and is at least 2, this implies occurrence of either or , i.e., 2.{, } _ {, }.
In this section, we consider bounded equal-conflict PT systems and show how to compute the relations introduced in Sec. 3 by exploiting the equal-conflict structure of the net.
The relations in Sec. 3 consider the unfolding of a system Unf(Σ) and analyse their
maximal configurations checking footprints, the multisets of transitions occurring in maximal
configurations. Here, we consider maximal-step semantics, since, as recalled in Sec. 2, it is
equivalent to step semantics in the case of equal-conflict systems, where there is no asymmetric
confusion [
Moreover, thanks to the results in [
In fact, in [
In the case of occurrence sequences, the equivalence relation abstracts w.r.t. the total order arbitrarily chosen when transitions are concurrent; in the case of processes, the equivalence abstracts from the distinction among several tokens on the same place.
From the construction of the equivalence classes both of occurrence sequences and of processes, it is possible to observe that the elements in each class have the same footprints, i.e., the same multiset of transitions which can be observed through the corresponding behaviour, and that elements of an equivalence class in bijective correspondence with a class of the other sort have the same footprint too.
Given this correspondence, in the next subsections we introduce a tree, whose paths record the set of maximal-step sequences of Σ, and show that a particular prefix of this tree is suficient to compute the reveals relations. Note that since we are interested in maximal configurations, we cannot directly work on the marking graph of the net, since its maximal paths are not necessarily associated with maximal configurations in the unfolding.
The tree and its prefix were first introduced in [
Definition 6. Let Σ = (, , , , 0) be a bounded equal-conflict PT system. We define the tree of maximal-step computations, denoted as msct(Σ) or msc-tree, as follows. • Each node of the tree is labelled with a reachable marking. • The root of the tree is labelled with the initial marking 0. • From each node labelled with marking , for each maximal step enabled at , there is an outgoing arc, labelled with , and leading to a node labelled with ′, where [ ⟩′.
A path in msct(Σ) is a sequence = 1122 · · · , such that, for each , there is an arc from to +1, labelled with . A path is initial if it starts in the root of the tree. A path can be either finite or infinite. Let , be two nodes on the same path , < if is closer to the root than . The footprint of the path is the (multiset) union of all steps occurring in .
We define an inclusion relation between footprints: let 1 and 2 be paths on msct(Σ); then ( 1) ⊆ ( 2) if ∀ ∈ , ( 1)() ≤ ( 2)(), i.e., for each transition , the number of occurrences in the footprint of 1 is less than or equal to that in the footprint of 2.
To simplify the notation, we will write ∈ ( ) when ( )() ≥ 1, namely when occurs in some step of path .
From the considerations in the first part of Sec. 4, each maximal path in msct(Σ) can be associated to at least one maximal configuration of the unfolding, with the same footprint; and vice versa, each configuration of Unf(Σ) is represented in the msct(Σ) by a path with the same footprint.
Example 5. Fig. 6 represents a PT system and a prefix of its maximal computation tree. In the tree, the markings are represented as multisets of places. In each marking, if a place appears only once, its multiplicity is omitted; if a place appears times, for the sake of clarity in the figure, it is denoted with . For example, the initial marking of the net is represented with 1, 62. Note that the PT system is the same of Ex. 1, and in Fig. 2 a branching process of Σ is shown.
Let = {1, 2, ..., , ...} be the set of nodes in msct(Σ), and : → [0⟩ the labelling function, mapping to each node the corresponding marking. Two nodes 1 and 2 are equivalent if (1) = (2). Let 1 = 1122...... and 2 = 1′1′ 2′2′ ...′′... be two paths on the tree, where the elements represent nodes of the tree, and the elements represent the labels of the arcs. The path 1 is isomorphic to the path 2 (in symbols 1 ≃ 2) if for each , ( ) = (′ ), and ( ) = (′ ). Finally, two subtrees 1 and 2 are isomorphic if for each maximal path on 1 there is a maximal path ′ in 2 such that ≃ ′, and vice versa.
Let be a maximal path on the tree, and one of its nodes. We denote with ↓ () the path from the root to , and with ↑ () the subpath starting from .
Lemma 1. Let and be two nodes of an msc-tree such that () = (). The subtree with as root and the one with as root are isomorphic.
Proof. Since () = (), the arcs leaving from and from have the same labels. Then, by construction the children of are equivalent to the children of , and the same reasoning can be applied to each of them.
On the maximal paths of the msc-tree, we can define a peeling operation as follows [
In this section we recall the definition of full prefix given in [ useful when presenting the algorithm.
18] and some results that will be Definition 7. Let Σ be a bounded equal-conflict PT system. The full prefix of msct (Σ), denoted fp(Σ), is a labelled rooted tree defined by the following clauses.
2. Let be a node of fp(Σ). If there is no ′ such that ′ < and (′) = (), then all the children of in the msct (Σ) are nodes in fp(Σ); otherwise is a leaf in fp(Σ). Example 6. The tree in Fig. 6 is a full prefix. Each node is labelled with a marking, and each arc is labelled with a multiset of transitions. The leaves are either deadlocks, and in this case they are denoted with a black thick line, or repeated markings, and in this case the leaves are in the same colour of the node that they repeat. Moreover, some nodes have a second label: in particular, the leaves are labelled with , ∈ {1, ..., 8}, and, for each leaf corresponding to a repeated marking labelled with , its repetition is labelled rep().
The full prefix fp(Σ) is finite, since the length of a path cannot exceed the number of markings of the net system, and every node has a finite number of children.
For each maximal path on = fp(Σ), we will denote with ( ) the leaf of the path, and, if ( ) is not a deadlock, we will denote as rep(( )) the node preceding ( ) and such that (( )) = (rep(( ))). In addition, we will denote as rep(( )) the subtree of with root rep(( )).
Lemma 2. Let be a path on msct (Σ), and ∈ a transition. If ≤ ( )(), but ̸∈ ∩ fp(Σ), then there is another path ′ ∈ msct (Σ) such that ( ′) ⊆ ( ), ≤ ( ′)(), and ∈ ′ ∩ fp(Σ).
Proof. Let ( 1) be the leaf of 1 = ∩ fp(Σ) and rep(( 1)) its repetition in the prefix. We can construct the run 1′ = (, rep(( 1)),( 1)). If ∈ 2 = 1′ ∩ fp(Σ) we can stop the construction, otherwise we repeat the procedure by considering ( 2). Since the distance between the root and the first occurrence of is finite, and every step of the peeling reduces it, after a finite number of peeling operations the thesis must be satisfied.
Let ′ be a maximal path on msct(Σ), and its prefix on fp(Σ). If ( ) is not a deadlock, there must be a prefix of ′ extending with a segment isomorphic to another segment in fp(Σ) starting from rep(( )) and arriving to a leaf of fp(Σ). Let 1 be such a segment; we denote with + 1 the prefix of ′ obtained by concatenating with a segment isomorphic to 1. If ( 1) is not a deadlock, then + 1 can be extended further by looking in fp(Σ) which segments start from rep(( 1)). Among them, there must be a segment 2 such that + 1 can be extended with a segment isomorphic to 2, obtaining a longer prefix of ′: + 1 + 2.
Proceeding in this way, we can obtain an arbitrarily long prefix of ′ from fp(Σ).
In this section, we propose an algorithm to compute the collective reveals relation, defined in Def. 5, on a bounded equal-conflict PT system Σ, through the full prefix fp(Σ). Its pseudo-code is presented in Algorithm 1. Since reveals (Def. 1) and repeated reveals (Def. 3) can be expressed as special cases of collective reveals (see Remark 6), the algorithm allows to compute also these relations. At the end of the section, we will discuss how to modify it to compute also extended-repeated reveals (Def. 4).
Algorithm 1 takes as input the full prefix = fp(Σ), two sets of transitions, and , and a positive number . If there is no path in the msct(Σ) with at least occurrences of transitions of , then the algorithm returns undefined . Otherwise, it returns true if . _ , false if . ̸_ . The main function of the algorithm is repex. The variable ‘Paths’ includes all the prefixes of the paths of msct(Σ) that we need to check to verify the relation. Initially, it includes all the paths in fp(Σ) with at least an occurrence of a transition of (this is justified by Lemma 2). The variable ‘empty’ is true if a path with at least occurrences of transitions of has not been found, false otherwise. ‘Paths’ and ‘empty’ are the input arguments of the function extendPaths. This function checks which input paths already include at least occurrences of transitions of , and, if it finds a path with occurrences of and none of , it sets the value of ‘stop’ to true, and stops the execution. In this case, also the main function will stop, and return false, since the path could be extended to a maximal path of msct(Σ) without adding any new transition label. If the path has at least occurrences of and an occurrence in , then it does not need to be elongated further, and the algorithm must continue with the analysis of the other paths.
Let be a path with less than occurrences of ; then the algorithm needs to check which extensions could be useful to add more occurrences of transitions of . If ends with a deadlock, it is not possible to extend it further, and since there are no occurrences of we are not interested in it. Otherwise, rep(( )) is well defined, and all the paths extending are labelled as one of the paths starting from rep(( )). Let ext be any path starting from rep(( )). If does not have any occurrence of and ends with a deadlock, then we do not need to consider it, since the concatenation + of and does not have occurrences of . Also, we do not consider the extension of with no occurrence of , and such that rep(( )) ≤ rep(()), since each path with such a prefix and occurrences of can be peeled removing and still have occurrences of . All the other extensions are put in the variable ‘newPaths’, and will be considered in the next round. If there are no paths left to analyse, and in all those with at least occurrences of there is an occurrence in , then the algorithm returns true. Example 7. Consider the net in Fig. 6 and its full prefix. Assume that we want to check the relation 2.{, } _ {}. We can easily see that the relation is verified. The first part of the relation is satisfied if we observe or at least twice, or both and once. In all these cases, must have occurred to bring the token back in 1. We simulate some steps of the algorithm to see how to arrive at this conclusion. First, we need to consider all the paths with at least an occurrence of or of . In this case, these are all the paths of the full prefix. Since none of them has two occurrences, we need to check the possible extensions for all of them. The two paths ending in a deadlock cannot be extended further, therefore we can stop to consider them. In what follows, if a transition has multiplicity 1 in a footprint, we will omit the 1. Consider the path with footprint {, , 2.ℎ, , }. Its possible extensions are isomorphic to the segments starting with rep(2): these have labels { } and {, ℎ}. In none of them an occurrence of or appears; the segment labelled { } ends in a deadlock, and the leaf of the segment labelled {, ℎ} (2) coincides with rep(2), therefore none of these extensions is useful to observe a second occurrence in {, } and we can discard the path. Analogously for the path with footprint {, , , , , 2.ℎ}. A similar reasoning Algorithm 1 Computing collective reveals function (: full prefix, , ⊆ , ∈ N) ∈ {true, false, undefined } Paths = The list of maximal paths in with at least an element of empty = True while Paths ̸= []
Paths, empty, stop = ℎ(Paths, empty) if stop == true
return false end if end while if empty == true
return undefined else
return true end if end function function ℎ(Paths, empty) # returns a triple (, , ), where is a list of paths, and and are boolean values newPaths = [] for ∈ Paths if | ∩ | ≥ empty = false if ∩ == ∅
return [], false, true end if else if ( ) is not a deadlock for ∈ (( )) if ∩ ̸= ∅ ∨ ((()) < (( )))
newPaths.append( + ) end if end for end if end for return newPaths, empty, false end function # | ∩ | is equivalent to ∑︀∈ ( )() can be done for the paths with footprints {, , ℎ, } and {, , , ℎ, }: in these cases, the possible extensions start from the nodes rep(6) and rep(4) respectively, but none of them has an other occurrence of or , and the repetition of the non-deadlock leaves coincides or follows these nodes. Hence, the only paths that we can extend are those ending with the nodes 7 and 5 ({, } and {, , } respectively). The extensions of these paths start from the root, therefore in all of them there is an occurrence of or one of , and these extended paths have two occurrences in {, }. Since in all of them there is already an occurrence of , we can stop, and conclude 2.{, } _ {}. Lemma 3. The leaf of every path constructed by the algorithm is a deadlock, or is associated with a marking that is already present in the path.
Proof. First we observe that every path constructed by the algorithm ends with a node equivalent to a leaf in the prefix tree. For each leaf, the path in the tree starting from the root and arriving to it is unique.
Let be the root of the tree, 0 1′... ′ be a path constructed by the algorithm, where 0 is a maximal path in the prefix tree and ′ is an added segment isomorphic to a segment starting from rep(( − 1)) (the repetition of the leaf ( − 1) of the segment − 1) and ending in ( ), a leaf of the prefix tree. We have to prove that, if the leaf of the constructed path is not a deadlock, then the repetition rep(( ′)) of the leaf ( ′) of the path belongs to the path itself, i.e., rep(( ′)) is in 0 1′... ′.
We prove it by induction. Let ( 1′) be the leaf of 0 1′; if it is not a deadlock, then rep(( 1′)) is either in 1′ or inside [, rep(( 0))], where [, rep(( 0))] is the path from the root to the repetition of the leaf of 0 and then it is contained in 0. Then rep(( 1′)) ∈ 0 1′.
We now assume the constructed path 0 1′... ′ ends either with a deadlock, or with a node whose repetition rep(( ′)) is either in ′ or in the segment [, rep(( ′− 1))], which is contained in 0 1′... ′− 1, and then rep(( ′)) ∈ 0 1′... ′.
We prove that the path 0 1′... ′+1 ends either with a deadlock, or with a node whose repetition rep(( ′+1)) is either in ′+1 or in the segment [, rep(( ′))], which is contained in 0 1′... ′, and therefore rep(( ′+1)) ∈ 0 1′... ′+1. In fact, ′+1 is isomorphic to a segment +1 in the prefix tree starting from rep(( )), which is between and ( ), and ending in a leaf ( +1) of the prefix tree. This last leaf is either a deadlock, or has a repetition, which is either in +1 or in [, rep(( ))]; since rep(( ′)) is by inductive hypothesis in 0 1′... ′, we get the thesis.
Lemma 4. Let be any maximal path in the msc-tree. If has in total at least occurrences of transitions belonging to , then there is at least a path ′ analysed by the algorithm with in total at least occurrences of transitions of , such that ( ′) ⊆ ( ).
Proof. We show that we can peel and obtain a maximal path of the msc-tree such that its prefix is analysed. For Lemma 2, we can peel and obtain a path 1 such that at least an occurrence of appears in its prefix in fp(Σ). Let 1′ be such prefix. If 1′ has occurrences of , we don’t need to proceed further; otherwise 1′ must be followed in 1 by a path isomorphic to a path starting from rep(( 1′)). Let 2′ be this segment. If 2′ has at least an occurrence of a transition of , or rep(( 2′)) precedes rep(( 1′)), this elongation of the prefix has been considered by the algorithm. If 2′ has no occurrences of and rep(( 2′)) ≥ rep(( 1′)), then we can peel 1 of the part between rep(( 2′)) and ( 2′), obtaining 12. Since in 2′ there are no elements of , this cannot influence their number in 12, and ( 12) ⊆ ( 1). The path 12 has also a prefix made by 1′ concatenated with a segment starting from rep(( 1′)). Let 3′ be this segment. If rep(( 3′)) ≥ rep(( 1′)), we repeat the peeling procedure. Since 1 has occurrence of by hypothesis, after a finite number of steps, we will obtain a peeled maximal run 1 such that rep(( ′)) < rep(( 1′)), with ′ segment starting from rep(( 1′)) elongating the segment 1′, or ′ has at least an occurrence of . We can repeat this reasoning until obtaining a prefix with at least occurrences of . Since in our steps we never remove any of those, and includes them by hypothesis, this procedure ends after a finite number of steps. By construction, all the transitions in the constructed prefix are also in , therefore we produced a prefix as required from the thesis.
Proof. As first step we show that if the algorithm returns false, then . ̸_ . The algorithm returns false if the variable ‘stop’ is true. The value of ‘stop’ is selected into the function extendPaths, and it is set to true if a path is found with occurrences of and none in . Each prefix is constructed so that the final leaf is a deadlock for the path, or it is repeated previously; in the first case the path is already maximal, in the second case, the path can be extended to a maximal path without adding any new transition by repeating infinitely often the segment between the leaf of the prefix and its repetition. The existence of such a repetition is guaranteed by Lemma 3. In both cases there is a maximal run with at least occurrences of and none in , therefore . ̸_ .
We now show that if the algorithm returns true, then . _ . This is a consequence of Lemma 4: if there were a path with occurrences of and none in , Lemma 4 guarantees that we would analyse a prefix with the same feature, but if this happens, the algorithm returns false. If the algorithm returns undefined, then there cannot be any run in the msc-tree with occurrences of transitions of as a consequence of Lemma 4.
Proof. The algorithm ends when the variable ‘Paths’ becomes empty, or when a path with
occurrences of and none in was found. We show that ‘Paths’ becomes empty after a finite
number of steps. The variable ‘Paths’ is a list of prefixes of paths in the msc-tree. Its content in
each iteration of the while loop is entirely determined by the function extendPaths, that elongate
some of its elements. In particular, the function elongates the paths with less of occurrences
of . Each path can be elongated in two ways: adding at least an additional occurrence of ,
and this happens only finitely many times, since when the path has at least occurrences of
it is not extended anymore, or with a segment whose repetition of the leaf is strictly closer
to the root than the repetition of the previous leaf. Also in this second case the number of
extension is finite, since the distance between each node and the root is finite.
Remark 7. To compute the reveals relation, the algorithm needs to analyse only the maximal
runs of the prefix tree, without further extensions. This is coherent with the result in [
Algorithm 1 can be adapted to compute the relation presented in Def. 4. Here we give only a sketch of how this can be done. Let = {1, ..., } and be the input sets. Instead of having just a single threshold in input as for repeated reveals, the input must include all the thresholds {1, ..., } related to transitions of , and the information about how they are associated to these transitions. Since the number of observations in which we are interested changes for every transition, when the algorithm needs to decide whether a path can stop or needs to be extended, it must consider all transitions of separately, each with its threshold. In addition, if a path has already reached the number of required occurrences of a certain transition, we should stop to consider this transition as useful when we evaluate the possible extensions.
Since extended reveals (Def. 2) can be expressed as a special case of extended-repeated reveals, modifying the algorithm as described would allow for its computation.
In this paper, we have introduced two new variants of reveals relation, namely extended-repeated reveals and collective reveals. The relations are defined for transitions of general PT nets and they express positive information flow. Existence of reveals relation (or its variants) between transitions means that the occurrence of one gives information about the other one. It can violate security of a system when a low transition reveals a high transition. The new variants introduced in this paper are parametric and they allow one to specify security requirements of a distributed system based on the specific needs of the system. They provide scalability by allowing one to specify diferent levels of security.
Building upon the results from [
One of our next steps will be performing a complexity analysis of the proposed methods and
working on improving the eficiency. This includes investigation of a shorter prefix and more
eficient algorithms. We plan to work on extending our results to more general classes of Petri
nets such as unbounded equal-conflict PT systems. We will explore the practical use of our
methods for both information-flow analysis and verification of other desired behavioural properties
of complex distributed systems. We will also explore diferent approaches to information-flow
analysis on Petri nets by considering games like in [
This work is partially supported by the Italian MUR.