{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T04:18:14Z","timestamp":1746159494263,"version":"3.40.4"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031866944","type":"print"},{"value":"9783031866951","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-86695-1_2","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:50Z","timestamp":1746151610000},"page":"15-27","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Verifying Security Policies for\u00a0Infinite-State Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-3150-0226","authenticated-orcid":false,"given":"Quentin","family":"Peyras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-0871-0767","authenticated-orcid":false,"given":"Ghada","family":"Gharbi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8140-0273","authenticated-orcid":false,"given":"Souheib","family":"Baarir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,5,3]]},"reference":[{"issue":"2\u20133","key":"2_CR1","first-page":"137","volume":"54","author":"R Barbuti","year":"2003","unstructured":"Barbuti, R., Tesei, L.: A decidable notion of timed non-interference. Fund. Inform. 54(2\u20133), 137\u2013150 (2003)","journal-title":"Fund. Inform."},{"key":"2_CR2","unstructured":"Bell, D., Padula, L.: Secure Computer Systems: Mathematical Foundations and Model. Mitre Corporation (1973). https:\/\/books.google.fr\/books?id=y_SNPAAACAAJ"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-031-13185-1_17","volume-title":"Computer Aided Verification","author":"R Beutner","year":"2022","unstructured":"Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification, pp. 341\u2013362. Springer, Cham (2022)"},{"key":"2_CR4","doi-asserted-by":"publisher","unstructured":"Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281\u2013283 (1979). https:\/\/doi.org\/10.1145\/359104.359108","DOI":"10.1145\/359104.359108"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. CoRR abs\/1401.4492 (2014). http:\/\/arxiv.org\/abs\/1401.4492","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: 2008 21st IEEE Computer Security Foundations Symposium, pp. 51\u201365 (2008). https:\/\/doi.org\/10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Conchon, S., Goel, A., Krstic, S., Mebsout, A., Za\u00efdi, F.: Cubicle: a parallel smt-based model checker for parameterized systems - tool paper. In: CAV, pp. 718\u2013724 (2012)","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Dardinier, T., M\u00fcller, P.: Hyper hoare logic: (dis-)proving program hyperproperties. In: Proceedings of the ACM on Programming Languages, vol. 8, pp. 1485\u20131509 (2024). https:\/\/doi.org\/10.1145\/3656437","DOI":"10.1145\/3656437"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Dickerson, R., Ye, Q., Zhang, M.K., Delaware, B.: RHLE: modular deductive verification of relational $$\\forall \\exists $$ properties. In: Programming Languages and Systems: 20th Asian Symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, Proceedings, pp. 67\u201387. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-21037-2_4","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B.: Temporal hyperproperties. Bull. EATCS 123 (2017)","DOI":"10.1007\/978-3-319-67531-2_12"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Frenkel, H., Hofmann, J., Lohse, J.: Automata-based software model checking of hyperproperties (2023)","DOI":"10.1007\/978-3-031-33170-1_22"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., M\u00fcller, C., Seidl, H., Z\u0103linescu, E.: Verifying security policies in multi-agent workflows with loops. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. pp. 633\u2013645. CCS 2017. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134080","DOI":"10.1145\/3133956.3134080"},{"key":"2_CR13","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. CoRR abs\/1610.04388 (2016). http:\/\/arxiv.org\/abs\/1610.04388"},{"issue":"1","key":"2_CR14","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1109\/JSAC.2002.806122","volume":"21","author":"R Focardi","year":"2003","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Real-time information flow analysis. IEEE J. Sel. Areas Commun. 21(1), 20\u201335 (2003). https:\/\/doi.org\/10.1109\/JSAC.2002.806122","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Gardey, G., Mullins, J., Roux, O.H.: Non-interference control synthesis for security timed automata. Electronic Notes in Theoretical Computer Science 180(1), 35\u201353 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2005.05.046, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066107003143, proceedings of the International Workshop on Security and Concurrency (SecCo 2005)","DOI":"10.1016\/j.entcs.2005.05.046"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Ghosal, S., Shyamasundar, R.K.: A generalized notion of non-interference for flow security of sequential and concurrent programs. In: 2020 27th Asia-Pacific Software Engineering Conference (APSEC), pp. 51\u201360 (2020). https:\/\/doi.org\/10.1109\/APSEC51365.2020.00013","DOI":"10.1109\/APSEC51365.2020.00013"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: 1982 IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982). https:\/\/doi.org\/10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"Lamport, L.: A simple approach to specifying concurrent systems. Commun. ACM 32(1), 32-45 (1989). https:\/\/doi.org\/10.1145\/63238.63240","DOI":"10.1145\/63238.63240"},{"key":"2_CR19","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc, USA (2002)"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Macedo, N., Brunel, J., Chemouil, D., Cunha, A., Kuperberg, D.: Lightweight specification and analysis of dynamic systems with rich configurations. In: Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering. pp. 373\u2013383. FSE 2016. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2950290.2950318","DOI":"10.1145\/2950290.2950318"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"M\u00fcller, C., Seidl, H., Z\u011flinescu, E.: Inductive invariants for noninterference in multi-agent workflows. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 247\u2013261 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00025","DOI":"10.1109\/CSF.2018.00025"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Padon, O., Hoenicke, J., Losa, G., Podelski, A., Sagiv, M., Shoham, S.: Reducing liveness to safety in first-order logic. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158114","DOI":"10.1145\/3158114"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: IVY: safety verification by interactive generalization. SIGPLAN Not. 51(6), 614\u2013630 (2016). https:\/\/doi.org\/10.1145\/2980983.2908118","DOI":"10.1145\/2980983.2908118"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Peyras, Q., Bodeveix, J.P., Brunel, J., Chemouil, D.: Sound verification procedures for temporal properties of infinite-state systems. In: Silva, A., Leino, K. (eds.) Computer Aided Verification, pp. 337\u2013360. Springer, Cham (2021)","DOI":"10.1007\/978-3-030-81688-9_16"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"issue":"1","key":"2_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5\u201319 (2003). https:\/\/doi.org\/10.1109\/JSAC.2002.806121","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"2_CR27","unstructured":"Zimmermann, J., Mohay, G.: Distributed intrusion detection in clusters based on non-interference. In: Proceedings of the 2006 Australasian Workshops on Grid Computing and E-Research, vol. 54. pp. 89\u201395. ACSW Frontiers 2006, Australian Computer Society, Inc. (2006)"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools and Experiments"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-86695-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T02:06:58Z","timestamp":1746151618000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-86695-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031866944","9783031866951"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-86695-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"3 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.soundandcomplete.org\/vstte2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}