带循环的多Agent工作流的安全策略
Verifying Security Policies in Multi-agent Workflows with Loops
摘要：
我们认为基于Web的工作流，如会议提交系统，如EasyChair的信息流安全策略的自动验证。我们的工作流描述语言允许循环，非确定性的选择，和无限数量的参与代理。信息流策略在超属性的时态逻辑中指定。我们证明了验证问题可以归结为一阶线性时间时序逻辑公式的可满足性，并为相关类别的工作流和规范提供可判定性结果。我们报告的一系列基准上实现我们的方法所获得的实验结果。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
