Abstract
We introduce two families of relations on the transitions of a Petri net. The first one is an adaptation of the “reveals” relation previously defined on occurrence nets for fault diagnosis applications. Here, this relation is considered for modeling positive information flow, which arises when the occurrence of a transition gives the information that another transition already occurred or will occur. The second one, called “excludes”, is presented for modeling negative information flow, which arises when the occurrence of a transition gives information on the non-occurrence of another transition, in the past or in the future. We consider the notion of non-interference proposed in the literature for formalizing security in distributed systems. On the basis of reveals and excludes relations we propose a collection of new notions of non-interference for ordinary Petri nets and compare them with notions already proposed in the literature.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Balaguer, S., Chatain, T., Haar, S.: Building tight occurrence nets from reveals relations. In: Caillaud, B., Carmona, J., Hiraishi, K. (eds.) 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, pp. 44–53. IEEE, 20–24 June 2011. http://doi.ieeecomputersociety.org/10.1109/ACSD.2011.16
Balaguer, S., Chatain, T., Haar, S.: Building occurrence nets from reveals relations. Fundam. Inform. 123(3), 245–272 (2013). http://dx.doi.org/10.3233/FI-2013-809
Baldan, P., Carraro, A.: Non-interference by unfolding. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 190–209. Springer, Heidelberg (2014)
Bernardinello, L., Kılınç, G., Pomello, L.: Non-interference notions based on reveals and excludes relations for Petri nets. In: Proceedings of the International Workshop on Petri Nets and Software Engineering (PNSE 2015), Brussels, Belgium, pp. 59–78, 22–23 June 2015
Best, E., Darondeau, P.: Deciding selective declassification of Petri nets. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 290–308. Springer, Heidelberg (2012)
Best, E., Darondeau, P., Gorrieri, R.: On the decidability of non interference over unbounded Petri nets. In: Chatzikokolakis, K., Cortier, V. (eds.) Proceedings 8th International Workshop on Security Issues in Concurrency, SecCo 2010, Paris, France, vol. 51, pp. 16–33. EPTCS, 30 August 2010. http://dx.doi.org/10.4204/EPTCS.51.2
Bryans, J., Koutny, M., Mazaré, L., Ryan, P.Y.A.: Opacity generalised to transition systems. Int. J. Inf. Sec. 7(6), 421–435 (2008). http://dx.doi.org/10.1007/s10207-008-0058-x
Bryans, J., Koutny, M., Ryan, P.Y.A.: Modelling opacity using Petri nets. Electr. Notes Theor. Comput. Sci. 121, 101–115 (2005). http://dx.doi.org/10.1016/j.entcs.2004.10.010
Busi, N., Gorrieri, R.: A survey on non-interference with Petri nets. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 328–344. Springer, Heidelberg (2004)
Busi, N., Gorrieri, R.: Positive non-interference in elementary and trace nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 1–16. Springer, Heidelberg (2004)
Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991). http://dx.doi.org/10.1007/BF01463946
Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. J. Comput. Secur. 3(1), 5–34 (1995)
Focardi, R., Gorrieri, R.: Classification of security properties (Part I: information flow). In: FOSAD [14], pp. 331–396
Focardi, R., Gorrieri, R. (eds.): FOSAD 2000. LNCS, vol. 2171, pp. 331–396. Springer, Heidelberg (2001)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)
Gorrieri, R., Vernali, M.: On intransitive non-interference in some models of concurrency. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol. 6858, pp. 125–151. Springer, Heidelberg (2011)
Haar, S.: Unfold and cover: qualitative diagnosability for Petri nets. In: Proceedings of 46th IEEE Conference on Decision and Control (2007)
Haar, S., Rodríguez, C., Schwoon, S.: Reveal your faults: it’s only fair! In: Carmona, J., Lazarescu, M.T., Pietkiewicz-Koutny, M. (eds.) 13th International Conference on Application of Concurrency to System Design, ACSD 2013, Barcelona, Spain, pp. 120–129. IEEE, 8–10 July 2013. http://dx.doi.org/10.1109/ACSD.2013.15
Kılınç, G.: Formal notions of non-interference and liveness for distributed systems. Ph.D. thesis, Universitdegli Studi di Milano-Bicocca (2015)
Mazaré, L.: Using unification for opacity properties. In: Proceedings of WITS, pp. 165–176 (2004)
Roscoe, A.W.: CSP and determinism in security modelling. In: IEEE Symposium on Security and Privacy, pp. 114–127. IEEE Computer Society (1995)
Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report. http://www.csl.sri.com/papers/csl-92-2/
Ryan, P.Y.A.: Mathematical models of computer security. In: Focardi, R., Gorrieri, R. (eds.) [14], pp. 1–62
Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. In: CSFW, pp. 214–227. IEEE Computer Society (1999)
Schneider, S., Sidiropoulous, A.: CSP and anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)
Sutherland, D.: A model of information. In: Proceedings of National Computer Security Conference, pp. 175–183 (1986)
Acknowledgements
This work was partially supported by MIUR and by MIUR - PRIN 2010/2011 grant ‘Automi e Linguaggi Formali: Aspetti Matematici e Applicativi’, code H41J12000190001.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Bernardinello, L., Kılınç, G., Pomello, L. (2016). Non-interference Notions Based on Reveals and Excludes Relations for Petri Nets. In: Koutny, M., Desel, J., Kleijn, J. (eds) Transactions on Petri Nets and Other Models of Concurrency XI. Lecture Notes in Computer Science(), vol 9930. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53401-4_3
Download citation
DOI: https://doi.org/10.1007/978-3-662-53401-4_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-53400-7
Online ISBN: 978-3-662-53401-4
eBook Packages: Computer ScienceComputer Science (R0)