Web Services Verification and Prudent Implementation

Tigran Avanesov 1 Yannick Chevalier 2 Mohammed Anis Mekki 1 Michael Rusinowitch 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Alice&Bob notation is widely used to describe conversations between partners in security protocols. We present a tool that compiles an Alice&Bob description of a Web Services choreography into a set of servlets. For that we first compute for each partner an executable specification as prudent as possible of her role in the choreography. This specification is expressed in ASLan language, a formal language designed for modeling Web Services tied with security policies. Then we can check with automatic tools that this ASLan specification verifies some required security properties such as secrecy and authentication. If no flaw is found, we compile the specification into Java servlets that real partners can use to execute the choreography.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00641326
Contributor : Tigran Avanesov <>
Submitted on : Tuesday, November 15, 2011 - 2:28:37 PM
Last modification on : Thursday, June 27, 2019 - 4:27:42 PM
Long-term archiving on : Friday, November 16, 2012 - 10:56:36 AM

File

setop2011_submission_22.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00641326, version 1

Citation

Tigran Avanesov, Yannick Chevalier, Mohammed Anis Mekki, Michael Rusinowitch. Web Services Verification and Prudent Implementation. 4th SETOP International Workshop on Autonomous and Spontaneous Security, Sep 2011, Leuven, Belgium. ⟨hal-00641326⟩

Share

Metrics

Record views

572

Files downloads

289