{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T07:50:40Z","timestamp":1758268240087,"version":"3.40.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319153162"},{"type":"electronic","value":"9783319153179"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15317-9_17","type":"book-chapter","created":{"date-parts":[[2015,1,29]],"date-time":"2015-01-29T06:05:37Z","timestamp":1422511537000},"page":"269-287","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Intransitive Non-Interference by Unfolding"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Francesco","family":"Burato","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Carraro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,1,30]]},"reference":[{"issue":"5","key":"17_CR1","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236\u2013243 (1976)","journal-title":"Commun. ACM"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Rushby, J.M.: Design and verification of secure systems. In: SOSP 1981, pp. 12\u201321. ACM (1981)","DOI":"10.1145\/1067627.806586"},{"issue":"2","key":"17_CR4","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1109\/TSE.1987.226478","volume":"13","author":"JT Haigh","year":"1987","unstructured":"Haigh, J.T., Young, W.D.: Extending the noninterference version of mls for sat. IEEE Trans. Softw. Eng. 13(2), 141\u2013150 (1987)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"17_CR5","unstructured":"Rushby, J.: Noninterference, transitivity and channel-control security policies. Technical report. Technical report CSL-92-02, SRI International (1992)"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-540-30477-7_9","volume-title":"Programming Languages and Systems","author":"H Mantel","year":"2004","unstructured":"Mantel, H., Sands, D.: Controlled declassification based on intransitive noninterference. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 129\u2013145. Springer, Heidelberg (2004)"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Bossi, A., Piazza, C., Rossi, S.: Modelling downgrading in information flow security. In: CSFW2004, pp. 187\u2013201. IEEE (2004)","DOI":"10.1109\/CSFW.2004.1310741"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Best, E., Darondeau, P., Gorrieri, R.: On the decidability of non interference over unbounded Petri nets. In: SecCo 2010. EPTCS, vol. 51, pp. 16\u201333 (2010)","DOI":"10.4204\/EPTCS.51.2"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-23082-0_5","volume-title":"Foundations of Security Analysis and Design VI","author":"R Gorrieri","year":"2011","unstructured":"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\u2013151. Springer, Heidelberg (2011)"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-24631-2_4","volume-title":"Foundations of Security Analysis and Design II","author":"R Focardi","year":"2004","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2001. LNCS, vol. 2946, pp. 139\u2013185. Springer, Heidelberg (2004)"},{"key":"17_CR11","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: IEEE Symposium on Security and Privacy, pp. 178\u2013186. IEEE (1988)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Wittbold, J., Johnson, D.: Information flow in nondeterministic systems. In: IEEE Symposium on Security and Privacy, pp. 148\u2013161. IEEE (1990)","DOI":"10.1109\/RISP.1990.63846"},{"issue":"1\/2","key":"17_CR13","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/JCS-2001-91-204","volume":"9","author":"P Ryan","year":"2001","unstructured":"Ryan, P., Schneider, Y.: Process algebra and non-interference. J. Comput. Secur. 9(1\/2), 75\u2013103 (2001)","journal-title":"J. Comput. Secur."},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Mantel, H.: Possibilistic definitions of security - an assembly kit. In: CSFW 2000, pp. 185\u2013199. IEEE (2000)","DOI":"10.1109\/CSFW.2000.856936"},{"issue":"6","key":"17_CR15","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.1017\/S0960129509990120","volume":"19","author":"N Busi","year":"2009","unstructured":"Busi, N., Gorrieri, R.: Structural non-interference in elementary and trace nets. Math. Struct. Comput. Sci. 19(6), 1065\u20131090 (2009)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-07734-5_11","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"P Baldan","year":"2014","unstructured":"Baldan, P., Carraro, A.: Non-interference by unfolding. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 190\u2013209. Springer, Heidelberg (2014)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M Nielsen","year":"1981","unstructured":"Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part 1. Theor. Comput. Sci. 13, 85\u2013108 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR18","unstructured":"Esparza, J., Heljanko, K.: Unfoldings - A Partial order Approach to Model Checking. EACTS Monographs in Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"17_CR19","unstructured":"Baldan, P., Burato, F., Carraro, A.: UBIC2: unfolding-based interference checker 2 (2014). https:\/\/bitbucket.org\/fburato\/ubic2\/"},{"key":"17_CR20","unstructured":"Technology, S.: ANICA: automated non-interference check assistant (2011). http:\/\/service-technology.org\/anica"},{"issue":"1","key":"17_CR21","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF01384314","volume":"6","author":"KL McMillan","year":"1995","unstructured":"McMillan, K.L.: A technique of state space search based on unfolding. Formal Meth. Syst. Des. 6(1), 45\u201365 (1995)","journal-title":"Formal Meth. Syst. Des."},{"key":"17_CR22","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/s00236-003-0122-y","volume":"40","author":"V Khomenko","year":"2003","unstructured":"Khomenko, V., Koutny, M., Vogler, W.: Canonical prefixes of Petri net unfoldings. Acta Informatica 40, 95\u2013118 (2003)","journal-title":"Acta Informatica"},{"key":"17_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-319-02444-8_42","volume-title":"Automated Technology for Verification and Analysis","author":"C Rodr\u00edguez","year":"2013","unstructured":"Rodr\u00edguez, C., Schwoon, S.: Cunf: a tool for unfolding and verifying Petri nets with read arcs. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 492\u2013495. Springer, Heidelberg (2013)"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/BFb0039047","volume-title":"Proceedings of CONCUR 1990","author":"R Gorrieri","year":"1990","unstructured":"Gorrieri, R., Montanari, U.: SCONE: a simple calculus of nets. CONCUR 1990. LNCS, vol. 458, pp. 2\u201331. Springer, Heidelberg (1990)"},{"issue":"4\u20135","key":"17_CR25","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/s00165-008-0079-2","volume":"20","author":"R Devillers","year":"2008","unstructured":"Devillers, R., Klaudel, H., Koutny, M.: A compositional Petri net translation of general pi-calculus terms. Formal Aspects Comput. 20(4\u20135), 429\u2013450 (2008)","journal-title":"Formal Aspects Comput."},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-32940-1_31","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"R Meyer","year":"2012","unstructured":"Meyer, R., Khomenko, V., H\u00fcchting, R.: A polynomial translation of $$\\pi $$-calculus (FCP) to safe Petri nets. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 440\u2013455. Springer, Heidelberg (2012)"},{"issue":"1","key":"17_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2012.04.046","volume":"449","author":"P Baldan","year":"2012","unstructured":"Baldan, P., Corradini, A., K\u00f6nig, B., Schwoon, S., Rodr\u00edguez, C.: Efficient unfolding of contextual Petri nets. Theor. Comput. Sci. 449(1), 2\u201322 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-28641-4_16","volume-title":"Principles of Security and Trust","author":"E Best","year":"2012","unstructured":"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\u2013308. Springer, Heidelberg (2012)"},{"key":"17_CR29","series-title":"IFIP International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/0-387-24098-5_12","volume-title":"Formal Aspects in Security and Trust","author":"J Bryans","year":"2005","unstructured":"Bryans, J., Koutny, M., Ryan, P.: Modelling dynamic opacity using Petri nets with silent actions. In: Dimitrakos, T., Martinelli, F. (eds.) FAST. IIFIP, vol. 173, pp. 159\u2013172. Springer, Heidelberg (2005)"},{"issue":"10","key":"17_CR30","doi-asserted-by":"publisher","first-page":"2310","DOI":"10.1109\/TAC.2010.2063490","volume":"55","author":"S Haar","year":"2010","unstructured":"Haar, S.: Types of asynchronous diagnosability and the reveals-relation in occurrence nets. IEEE Trans. Autom. Control 55(10), 2310\u20132320 (2010)","journal-title":"IEEE Trans. Autom. Control"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15317-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,17]],"date-time":"2025-05-17T23:23:52Z","timestamp":1747524232000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15317-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319153162","9783319153179"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15317-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"30 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}