Verifying Security Policies in Multi-Agent Workflows with Loops
| Title | Verifying Security Policies in Multi-Agent Workflows with Loops |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Finkbeiner, Bernd, Müller, Christian, Seidl, Helmut, Z\u alinescu, Eugen |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | composability, hyper first-order temporal logic, non-interference, pubcrawl, resilience, Resiliency, web of trust, workflows |
| Abstract | We consider the automatic verification of information flow security policies of web-based workflows, such as conference submission systems like EasyChair. Our workflow description language allows for loops, non-deterministic choice, and an unbounded number of participating agents. The information flow policies are specified in a temporal logic for hyperproperties. We show that the verification problem can be reduced to the satisfiability of a formula of first-order linear-time temporal logic, and provide decidability results for relevant classes of workflows and specifications. We report on experimental results obtained with an implementation of our approach on a series of benchmarks. |
| URL | https://dl.acm.org/doi/10.1145/3133956.3134080 |
| DOI | 10.1145/3133956.3134080 |
| Citation Key | finkbeiner_verifying_2017 |