Knowledge-theoretic approach to formal verification of Web services protocols
Guoxiang Yao, Qingliang Chen, Chanjuan Liu, Zhuolin Yang · 2010
Traditional formal methods for analyzing security protocols have gained great success to find attacks or prove their absence in the standard Dolev-Yao model. However, they cannot be applied directly to verify Web services protocols because of their inherent different message syntax. In this paper, we apply our justification-oriented and automatic formal approach again to verify directly security properties for a more complex Web services protocol, based on a fault-preserving mapping tool called SuD (SOAP under Dolev-Yao) and the well developed epistemic logic (logic of knowledge) as the underlying specification language. The effectiveness of the approach can be further confirmed by the experimental results.