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.
Note exceptional week day and room.
