Issue No. 01 - Jan.-Feb. (2017 vol. 10)
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
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).
Petri nets, Web services, Security, Special issues and sections, Protocols, Privacy, Business
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.