In distributed systems, the occurrence of an action can give information about the occurrence of other actions. This can be an unwanted situation when “high” actions of the system need to be kept secret, while allowing users to observe “low” actions. If it is possible to deduce information about occurrence of high actions by observing only low actions, then the system suffers from an unwanted information flow. “Reveals” and “excludes” relations were introduced for modelling and analysing such an information flow among actions of a distributed system that is modelled via Petri nets. In this paper, we provide a formal basis for computing reveals and excludes relations of 1-safe free-choice Petri nets. We introduce the “maximal-step computation tree” to represent the behaviour of a distributed system under maximal-step semantics. We define a finite prefix of the tree called “full prefix” and we show that it is adequate for analysing information flow by means of reveals and excludes relations.

Adobbati, F., Kılınç Soylu, G., Puerto, A. (2022). A Finite Prefix for Analysing Information Flow Among Transitions of a Free-Choice Net. IEEE ACCESS, 10, 38483-38501 [10.1109/ACCESS.2022.3165185].

A Finite Prefix for Analysing Information Flow Among Transitions of a Free-Choice Net

Adobbati F.;
2022

Abstract

In distributed systems, the occurrence of an action can give information about the occurrence of other actions. This can be an unwanted situation when “high” actions of the system need to be kept secret, while allowing users to observe “low” actions. If it is possible to deduce information about occurrence of high actions by observing only low actions, then the system suffers from an unwanted information flow. “Reveals” and “excludes” relations were introduced for modelling and analysing such an information flow among actions of a distributed system that is modelled via Petri nets. In this paper, we provide a formal basis for computing reveals and excludes relations of 1-safe free-choice Petri nets. We introduce the “maximal-step computation tree” to represent the behaviour of a distributed system under maximal-step semantics. We define a finite prefix of the tree called “full prefix” and we show that it is adequate for analysing information flow by means of reveals and excludes relations.
Articolo in rivista - Articolo scientifico
Analytical models; Computational modeling; concurrency; Concurrent computing; distributed systems; excludes relation; Finite element analysis; finite prefix; free-choice nets; full prefix; information flow; maximal-step computation tree; Petri nets; Petri nets; reveals relation; Security; Semantics;
English
38483
38501
19
Adobbati, F., Kılınç Soylu, G., Puerto, A. (2022). A Finite Prefix for Analysing Information Flow Among Transitions of a Free-Choice Net. IEEE ACCESS, 10, 38483-38501 [10.1109/ACCESS.2022.3165185].
Adobbati, F; Kılınç Soylu, G; Puerto, A
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10281/369938
Citazioni
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
Social impact