8481 articles  [english version]

inria-00133996, version 2

Toward an Automatic Analysis of Web Service Security

Yannick Chevalier a, 1, Denis Lugiez 2, Michael Rusinowitch () b, 3

N° RR-6341 (2007)

Résumé : Web services send and receive messages in XML syntax with some parts hashed, encrypted or signed, according to the WS-Security standard. In this paper we introduce a model to formally describe the protocols that underly these services, their security properties and the rewriting attacks they might be subject to. Unlike with usual security protocols, we have to address here the facts that: (1) The Web service receive/send actions are nondeterministic to accommodate the XML format and the lack of normalization in parsing XML messages. Our model is designed to permit non-deterministic operations. (2) The Web service message format is better modelled with multiset constructors than with fixed arity symbols. Hence we had to introduce an attacker model that handles associativecommutative operators. In particular we present a decision procedure for insecurity of Web services with messages built using encryption, signature, and other cryptographic primitives.

  • a –  Université Paul Sabatier - Toulouse III
  • b –  INRIA
  • 1 :  Institut de recherche en informatique de Toulouse (IRIT)
  • CNRS : UMR5505 – Institut National Polytechnique de Toulouse - INPT – Université des Sciences Sociales - Toulouse I – Université Toulouse I [UT1] Capitole – Université Toulouse le Mirail - Toulouse II – Université Paul Sabatier [UPS] - Toulouse III
  • 2 :  Laboratoire d'informatique Fondamentale de Marseille (LIF)
  • CNRS : UMR6166 – Université de la Méditerranée - Aix-Marseille II – Université de Provence - Aix-Marseille I
  • 3 :  CASSIS (INRIA Lorraine - LORIA / LIFC)
  • INRIA – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domaine : Informatique/Logique en informatique
  • Mots-clés : Security – web services – cryptographic protocols – combination of decision procedures – equational theories – rewriting
  • Référence interne : RR-6341
  • Versions disponibles :  v1 (28-02-2007) v2 (31-10-2007)
 
  • inria-00133996, version 2
  • http://hal.inria.fr/inria-00133996
  • oai:hal.inria.fr:inria-00133996
  • Contributeur : Rapport De Recherche Inria <>
  • Soumis le : Mercredi 31 Octobre 2007, 14:46:24
  • Dernière modification le : Mercredi 31 Octobre 2007, 14:48:06