2011 • In Data Privacy Management and Autonomous Spontaneus Security - 6th International Workshop, DPM 2011, and 4th International Workshop, SETOP 2011, Leuven, Belgium, September 15-16, 2011, Revised Selected Papers.
Web Services; Security Policy; Automated deployment
Abstract :
[en] 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.
Disciplines :
Computer science
Identifiers :
UNILU:UL-CONFERENCE-2012-440
Author, co-author :
Avanesov, Tigran ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Chevalier, Yannick
Anis Mekki, Mohammed
Rusinowitch, Michaël
Language :
English
Title :
Web Services Verification and Prudent Implementation
Publication date :
2011
Event name :
SETOP'11
Event place :
Leuven, Belgium
Event date :
September 15-16, 2011
Main work title :
Data Privacy Management and Autonomous Spontaneus Security - 6th International Workshop, DPM 2011, and 4th International Workshop, SETOP 2011, Leuven, Belgium, September 15-16, 2011, Revised Selected Papers.
Publisher :
Springer Berlin Heidelberg
ISBN/EAN :
978-3-642-28878-4
Pages :
173-189
Peer reviewed :
Peer reviewed
Commentary :
7122
Revised Selected Papers of 4th International Workshop, SETOP 2011
Network of Excellence on Engineering Secure Future Internet Software Services and Systems, NESSoS project, http://www.nessos-project.eu
Automated Validation of Trust and Security of Service-Oriented Architectures, AVANTSSAR project (2008-2010), http://www.avantssar.eu
AVANTSSAR. Deliverable 2.3: ASLan final version with dynamic service and policy composition (2010), http://www.avantssar.eu/pdf/deliverables/avantssar- d2-3.pdf
AVANTSSAR. Deliverable 5.4: Assessment of the AVANTSSAR Validation Platform (2010), http://www.avantssar.eu
AVANTSSAR. The AVANTSSAR Validation Platform (2010), http://www. avantssar.eu
AVISPA. Deliverable 2.3: The Intermediate Format (2003), http://www.avispa-project.org
Barros, A., Dumas, M., Oaks, P.: A Critical Overview of the Web Services Choreography Description Language (WS-CDL). BPTrends (2005)
Bhargavan, K., Corin, R., Deniélou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium, pp. 124-140. IEEE Computer Society, Washington, DC (2009)
Bieber, P.: A logic of communication in hostile environment. In: Proceedings of the Computer Security Foundations Workshop III, pp. 14-22 (June 1990)
Bultan, T., Su, J., Fu, X.: Analyzing conversations of web services. IEEE Internet Computing 10(1), 18-25 (2006)
Carbone, M., Honda, K., Yoshida, N.: Structured Communication-Centred Programming for Web Services. In: De Nicola, R. (Ed.) ESOP 2007. LNCS, Vol. 4421, pp. 2-17. Springer, Heidelberg (2007)
Carlsen, U.: Generating formal cryptographic protocol specifications. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pp. 137-146 (May 1994)
Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Orchestration under security constraints. In: Sixth International Workshop on Formal Aspects in Security and Trust (FAST 2009), Eindhoven, the Netherlands, November 5-6 (2009)
Chevalier, Y., Mekki, M.A., Rusinowitch, M.: Automatic composition of services with security policies. In: Proceedings of the 2008 IEEE Congress on Services - Part I, SERVICES 2008, pp. 529-537. IEEE Computer Society, Washington, DC (2008)
Chevalier, Y., Rusinowitch, M.: Compiling and securing cryptographic protocols. Inf. Process. Lett. 110(3), 116-122 (2010)
Denker, G., Millen, J.: CAPSL integrated protocol environment. In: DARPA Information Survivability Conference (DISCEX 2000), pp. 207-221. IEEE Computer Society (2000)
Fabrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, pp. 160-171 (May 1998)
Guttman, J.D., Herzog, J.C., Ramsdell, J.D., Sniffen, B.T.: Programming Cryptographic Protocols. In: De Nicola, R., Sangiorgi, D. (Eds.) TGC 2005. LNCS, Vol. 3705, pp. 116-145. Springer, Heidelberg (2005)
McCarthy, J., Krishnamurthi, S.: Trusted Multiplexing of Cryptographic Protocols. In: Degano, P., Guttman, J.D. (Eds.) FAST 2009. LNCS, Vol. 5983, pp. 217-232. Springer, Heidelberg (2010)
Millen, J., Muller, F.: Cryptographic protocol generation from CAPSL. Technical Report SRI-CSL-01-07, SRI International (December 2001)
Mödersheim, S.: Algebraic properties in alice and bob notation. In: ARES, pp. 433-440. IEEE Computer Society (2009)
Turuani, M.: The CL-Atse Protocol Analyser. In: Pfenning, F. (Ed.) RTA 2006. LNCS, Vol. 4098, pp. 277-286. Springer, Heidelberg (2006)
W3C Consortium. XML Path Language (XPath) 2.0, 2nd edn. December 14 (2010), http://www.w3.org/TR/xpath20/
World Wide Web Consortium. Web Services Choreography Description Language Version 1.0, November 9 (2005), http://www.w3.org/TR/ws-cdl-10/