Integrated Specification and Verification of Security Protocols and Policies
OPEN ACCESS
Loading...
Author / Producer
Date
2011
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
We propose a language for formal specification of service-oriented architectures. The language supports the integrated specification of communication level events, policy level decisions, and the interaction between the two. We show that the reachability problem is decidable for a fragment of service-oriented architectures. The decidable fragment is well suited for specifying, and reasoning about, security-sensitive architectures. In the decidable fragment, the attacker controls the communication media. The policies of services are centered around the trust application and trust delegation rules, and can
also express RBAC systems with role hierarchy. The fragment is of immediate practical relevance: We report on the specification and verification of two security-sensitive architectures, stemming from the e-government and e-health domains.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
Pages / Article No.
Publisher
ETH Zurich, Department of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science