Information Security Seminar 

17/06/2010, 16:15 — 17:15 — Room P4.35, Mathematics Building
Mohammad Torabi Dashti, ETH Zurich

Formal Specification and Verification of Security Services

A framework for specification and verification of security properties in service-oriented architectures is proposed. The framework encompasses communication level events and policy level decisions, and allows to reason about the interface between the two. A decision procedure is given for the reachability problem in a fragment of service-oriented architectures, where the Dolev-Yao attacker is in control of the communication level, and the policies of services belong to a certain subset of Horn theories. This subset is in particular sufficient for expressing typical RBAC systems with role hierarchy, as well as trust delegation and trust application.