TY - GEN
T1 - Specifying and verifying secrecy in workflows with arbitrarily many agents
AU - Finkbeiner, Bernd
AU - Seidl, Helmut
AU - Müller, Christian
N1 - Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016
Y1 - 2016
N2 - Web-based workflow management systems, like EasyChair, HealthVault, Ebay, or Amazon, often deal with confidential information such as the identity of reviewers, health data, or credit card numbers. Because the number of participants in the workflow is in principle unbounded, it is difficult to describe the information flow policy of such systems in specification languages that are limited to a fixed number of agents. We introduce a first-order version of HyperLTL, which allows us to express information flow requirements in workflows with arbitrarily many agents. We present a bounded model checking technique that reduces the violation of the information flow policy to the satisfiability of a first-order formula. We furthermore identify conditions under which the resulting satisfiability problem is guaranteed to be decidable.
AB - Web-based workflow management systems, like EasyChair, HealthVault, Ebay, or Amazon, often deal with confidential information such as the identity of reviewers, health data, or credit card numbers. Because the number of participants in the workflow is in principle unbounded, it is difficult to describe the information flow policy of such systems in specification languages that are limited to a fixed number of agents. We introduce a first-order version of HyperLTL, which allows us to express information flow requirements in workflows with arbitrarily many agents. We present a bounded model checking technique that reduces the violation of the information flow policy to the satisfiability of a first-order formula. We furthermore identify conditions under which the resulting satisfiability problem is guaranteed to be decidable.
UR - http://www.scopus.com/inward/record.url?scp=84992505815&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-46520-3_11
DO - 10.1007/978-3-319-46520-3_11
M3 - Conference contribution
AN - SCOPUS:84992505815
SN - 9783319465197
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 157
EP - 173
BT - Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Proceedings
A2 - Artho, Cyrille
A2 - Peled, Doron
A2 - Legay, Axel
PB - Springer Verlag
T2 - 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016
Y2 - 17 October 2016 through 20 October 2016
ER -