面向服务架构中授权策略和工作流的相互作用（完整版）
Verifying the Interplay of Authorization Policies and Workflow in Service-Oriented Architectures (Full version)
摘要：
在基于面向服务的范例的分布式应用中，一种广泛的设计方法，如Web服务，包括明确分离的授权策略和应用程序的工作流的执行，以便抽象出策略级别和工作流级别之间的相互作用。虽然这样的方法是有吸引力的，因为它是相当简单的，并允许一个原因的关键属性的政策正在考虑，它没有提供正确的抽象级别来指定和原因的方式工作流可能会干扰的政策，反之亦然。例如，作为工作流操作的副作用的证书的创建可能使策略规则能够触发并授予对特定资源的访问权;在不执行操作的情况下，策略规则应保持不活动状态。类似地，策略查询可以用作工作流转换的防护。在本文中，我们提出了一个两级形式化验证框架，以克服这些问题和形式化推理的授权策略和工作流在面向服务的体系结构中的相互作用。这使我们能够定义和调查一些验证问题的SO应用程序，并给出充分条件，其可判定性。
英文摘要：
A widespread design approach in distributed applications based on the service-oriented paradigm, such as web-services, consists of clearly separating the enforcement of authorization policies and the workflow of the applications, so that the interplay between the policy level and the workflow level is abstracted away. While such an approach is attractive because it is quite simple and permits one to reason about crucial properties of the policies under consideration, it does not provide the right level of abstraction to specify and reason about the way the workflow may interfere with the policies, and vice versa. For example, the creation of a certificate as a side effect of a workflow operation may enable a policy rule to fire and grant access to a certain resource; without executing the operation, the policy rule should remain inactive. Similarly, policy queries may be used as guards for workflow transitions. In this paper, we present a two-level formal verification framework to overcome these problems and formally reason about the interplay of authorization policies and workflow in service-oriented architectures. This allows us to define and investigate some verification problems for SO applications and give sufficient conditions for their decidability.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
