Abstract
Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet’s resolution-based protocol verifier. Hence, we can automatically verify authentication properties of SOAP protocols.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
[AF01] Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115 (2001)
[AG99] Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1–70 (1999)
[BEK+00] Box, D., Ehnebuske, D., Kakivaya, G., Layman, A., Mendelsohn, N., Nielsen, H., Thatte, S., Winer, D.: Simple Object Access Protocol (SOAP) 1.1, W3C Note NOTE-SOAP-20000508/ (2000), at http://www.w3.org/TR/2000/
[BFG04a] Bhargavan, K., Fournet, C., Gordon, A.D.: A semantics for web services authentication. In: 31st ACM Symposium on Principles of Programming Languages (POPL 2004), pp. 198–209 (2004)
[BFG04b] Bhargavan, K., Fournet, C., Gordon, A.D.: Verifying policy-based security for web services (Submitted 2004)
[Bla01] Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW-14), pp. 82–96. IEEE Computer Society, Los Alamitos (2001)
[Bla02] Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 342–359. Springer, Heidelberg (2002)
[Box01] Box, D.: A brief history of SOAP (2001), At http://webservices.xml.com/pub/a/ws/2001/04/04/soap.html
[BS03] Bierman, G., Sewell, P.: Iota: a concurrent XML scripting language with application to Home Area Networks. Technical Report 557, University of Cambridge Computer Laboratory (2003)
[DHK+04] Davis, M., Hartman, B., Kaler, C., Nadalin, A., Schwarz, J.: WS–I Security Scenarios, Working Group Draft Version 0.15 (February 2004), at http://www.ws-i.org/Profiles/BasicSecurity/2004-02/SecurityScenarios-0.15-WGD.pdf
[DY83] Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT–29(2), 198–208 (1983)
[GJ03] Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–521 (2003)
[GM03] Gardner, P., Maffeis, S.: Modelling dynamic web data. In: Lausen, G., Suciu, D. (eds.) DBPL 2003. LNCS, vol. 2921, pp. 130–146. Springer, Heidelberg (2003)
[GP03] Gordon, A.D., Pucella, R.: Validating a web service security abstraction by typing. In: ACM Workshop on XML Security 2002, pp. 18–29 (2003)
[HL03] Howard, M., LeBlanc, D.: Writing secure code, 2nd edn. Microsoft Press, Redmond (2003)
[IM02] IBM Corporation and Microsoft Corporation. Security in a web services world: A proposed architecture and roadmap (April 2002), At http://msdn.microsoft.com/library/en-us/dnwssecur/html/securitywhitepaper.asp
[JLLV04] Johnson, J.E., Langworthy, D.E., Lamport, L., Vogt, F.H.: Formal specification of a web services protocol. In: 1st International Workshop on Web Services and Formal Methods (WS-FM 2004), University of Pisa (2004)
[KN+04] Kaler, C., Nadalin, A., et al.: Web Services Secure Conversation Language (WS-SecureConversation) (May 2004), Version 1.1., At http://msdn.microsoft.com/ws/2004/04/ws-secure-conversation/
[Low97] Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of 10th IEEE Computer Security Foundations Workshop, pp. 31–44. IEEE Computer Society Press, Los Alamitos (1997)
[Mic02] Microsoft Corporation. Web Services Enhancements for Microsoft.NET (December 2002), At http://msdn.microsoft.com/webservices/building/wse/default.aspx
[Mil99] Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)
[NKHBM04] Nadalin, A., Kaler, C., Hallam-Baker, P., Monzillo, R.: OASIS Web Services Security: SOAP Message Security 1.0 (WS-Security (March 2004), At http://www.oasis-open.org/committees/download.php/5941/oasis-200401-wss-soap-message-security-1.0.pdf
[NS78] Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
[S+04] Schlimmer, J., et al.: A Proposal for UPnP 2.0 Device Architecture (May 2004), At http://msdn.microsoft.com/library/en-us/dnglobspec/html/devprof.asp
[SMWC03] Shewchuk, J., Millet, S., Wilson, H., Cole, D.: Expanding the communications capabilities of web services with WSAddressing (2003), At http://msdn.microsoft.com/library/default.asp?url=/library/en-us/dnwse/html/soapmail.asp
[SS02] Scambay, J., Shema, M.: Hacking Web Applications Exposed. McGraw-Hill/Osborne, New York (2002)
[Vog03] Vogels, W.: Web services are not distributed objects. IEEE Internet Computing 7(6), 59–66 (2003)
[W3C03] W3C. SOAP Version 1.2, W3C Recommendation (2003), at http://www.w3.org/TR/soap12
[Win98] Winer, D.: RPC over HTTP via XML (1998), At http://davenet.scripting.com/1998/02/27/rpcOverHttpViaXml
[Win99] Winer, D.: Dave’s history of SOAP (1999), At http://www.xmlrpc.com/discuss/msgReader$555
[WL93] Woo, T.Y.C., Lam, S.S.: A semantic model for authentication protocols. In: IEEE Computer Society Symposium on Research in Security and Privacy, pp. 178–194 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bhargavan, K., Fournet, C., Gordon, A.D., Pucella, R. (2004). TulaFale: A Security Tool for Web Services. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2003. Lecture Notes in Computer Science, vol 3188. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30101-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-30101-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22942-1
Online ISBN: 978-3-540-30101-1
eBook Packages: Springer Book Archive