Opacity Preserving Abstraction for Web Services and Their Composition Using SOGs

Automatic composition of Web services requires that the providers publish an abstract version of their Web services to a registry. They offer this abstraction instead of the complete Web service to ensure the privacy of their internal know-how and trade secrets. Many studies have offered methods to do this, but none of them is able to formally prove their ability to keep the secret information hidden. In this article we turn to the verification of opacity, a formal security property that allows not only to preserve the secret but also to formally prove that it remains hidden. In particular, we investigate if the composition of two opaque Web services is also opaque. Our work consists in verifying the opacity of the composition of two Web services through the verification of the opacity of their individual abstractions represented by Symbolic Observation Graphs.