Analysis And Verification Of The SOAP Security Based On Pi Calculus

XML-based web services technology is a new model of distributed computation. Its core message exchange protocol is SOAP (Simple Object Access Protocol). In the distributed environment, web services interact with each other via SOAP messages. Due to the flexibility of SOAP extensible mechanisms, web services may be vulnerable to certain attacks such as XML rewriting, although various standards like WS-Security and WS-Policy are theoretically suitable for ensuring end-to-end message level security.By analyzing some typical instances, it is known that because of lacking the description of SOAP topology in WS-Security, XML rewriting attack can modify the topology of SOAP message maliciously, for example, to insert bogus elements including bad codes, and then retransmit it without being detected by digital signature. The solution of the problem is adding additional SOAP Topology information into outgoing SOAP messages and validating this information before policy-driven validation at the receiving end. However, it s necessary to establish an end-to-end message level security model based on the solution above for processing a set of messages.The performance analysis result of this solution is satisfying. On the one hand, the extended XML security element does not occupy either more network bandwidth or additional CPU cycles at both the sender side and the receiver side. On the other hand, using Pi calculus, it is proved that this model is accord with security and authenticity. So,the security system that combines this solution and model is going to be the valid method for defending the XML rewriting attacks in web services.