The Community for Technology Leaders
Green Image
Issue No. 01 - Jan.-Feb. (2017 vol. 10)
ISSN: 1939-1374
pp: 66-79
Amina Bourouis , OASIS Reasearch Lab (ENIT), University of Tunis El Manar, Tunis, Tunisia
Kais Klai , LIPN, CNRS UMR 7030, University of Paris 13, Sorbonne Paris City, Villetaneuse, France
Nejib Ben Hadj-Alouane , OASIS Reasearch Lab (ENIT), University of Tunis El Manar, Tunis, Tunisia
Yamen El Touati , OASIS Reasearch Lab (ENIT), University of Tunis El Manar, Tunis, Tunisia
ABSTRACT
Web service (WS) providers need to restrain access to private information when cooperating with business partners. This need is translated in practice by an abstraction phase where inner data is withheld from public view. However, just like hiding encryption keys is not enough to prove the secrecy of information in a communication protocol, this procedure cannot prove the goal of secrecy is attained. Security related literature has turned in the past couple of decades to a new, formal, security property, i.e., opacity, to both hide and prove the privacy of secrets. Following our previous work on the use of the Symbolic Observation Graph (SOG), on one hand, to abstract and compose Web services, and to verify the opacity of systems on the other, we show in this paper how the verification of three different types of opacity in SOG-abstracted WSs is translated to the opacity of their composites. We hence establish that the SOG is a suitable abstraction that allows to check these opacity variants locally to each component of a composite WS, and preserves opacity by composition (i.e., each WS component is opaque iff the composite WS is).
INDEX TERMS
Petri nets, Web services, Security, Special issues and sections, Protocols, Privacy, Business
CITATION

A. Bourouis, K. Klai, N. B. Hadj-Alouane and Y. E. Touati, "On the Verification of Opacity in Web Services and Their Composition," in IEEE Transactions on Services Computing, vol. 10, no. 1, pp. 66-79, 2017.
doi:10.1109/TSC.2016.2605090
88 ms
(Ver 3.3 (11022016))