Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)
Cryptography and Security
2010-11-13 v1 Logic in Computer Science
Software Engineering
Abstract
We formalize automated analysis techniques for the validation of web services specified in BPEL and a RBAC variant tailored to BPEL. The idea is to use decidable fragments of first-order logic to describe the state space of a certain class of web services and then use state-of-the-art SMT solvers to handle their reachability problems. To assess the practical viability of our approach, we have developed a prototype tool implementing our techniques and applied it to a digital contract signing service inspired by an industrial case study.
Cite
@article{arxiv.1009.4625,
title = {Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC (Extended Version)},
author = {Alberto Calvi and Silvio Ranise and Luca Viganò},
journal= {arXiv preprint arXiv:1009.4625},
year = {2010}
}
Comments
12 pages, 3 figures, short version to appear in the Proceedings of WOSS'10, 1st Workshop on Software Services: Frameworks and Platforms