Verifying Security Policies in Multi-agent Workflows with Loops

TL;DR

This paper presents a method for automatically verifying information flow security policies in complex web-based workflows with loops and multiple agents, using a logical reduction approach.

Contribution

It introduces a workflow language with loops and non-determinism, and reduces verification to first-order linear-time temporal logic satisfiability, providing decidability results.

Findings

Decidability results for specific workflow classes

Implementation demonstrates practical verification on benchmarks

Logical reduction enables automated security policy verification

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.