Seminário Segurança de Informação 

15/10/2010, 16:15 — 17:15 — Sala P3.10, Pavilhão de Matemática
Luca Viganò, Università di Verona

Automated Validation of Security-sensitive Web Services specified in BPEL and RBAC

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. Joint Work with Alberto Calvi and Silvio Ranise.