TulaFale: A Security Tool for Web Services

  • Karthikeyan Bhargavan
  • Cédric Fournet
  • Andrew D. Gordon
  • Riccardo Pucella
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3188)


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.


Cryptographic Protocol Security Goal Security Tool Check Message IEEE Computer Security Foundation Workshop 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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)Google Scholar
  2. [AG99] Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1–70 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  3. [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
  4. [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)Google Scholar
  5. [BFG04b] Bhargavan, K., Fournet, C., Gordon, A.D.: Verifying policy-based security for web services (Submitted 2004)Google Scholar
  6. [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)Google Scholar
  7. [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)CrossRefGoogle Scholar
  8. [Box01] Box, D.: A brief history of SOAP (2001), At
  9. [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)Google Scholar
  10. [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
  11. [DY83] Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT–29(2), 198–208 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  12. [GJ03] Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security 11(4), 451–521 (2003)CrossRefGoogle Scholar
  13. [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)CrossRefGoogle Scholar
  14. [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)Google Scholar
  15. [HL03] Howard, M., LeBlanc, D.: Writing secure code, 2nd edn. Microsoft Press, Redmond (2003)Google Scholar
  16. [IM02] IBM Corporation and Microsoft Corporation. Security in a web services world: A proposed architecture and roadmap (April 2002), At
  17. [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)Google Scholar
  18. [KN+04] Kaler, C., Nadalin, A., et al.: Web Services Secure Conversation Language (WS-SecureConversation) (May 2004), Version 1.1., At
  19. [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)Google Scholar
  20. [Mic02] Microsoft Corporation. Web Services Enhancements for Microsoft.NET (December 2002), At
  21. [Mil99] Milner, R.: Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge (1999)zbMATHGoogle Scholar
  22. [NKHBM04] Nadalin, A., Kaler, C., Hallam-Baker, P., Monzillo, R.: OASIS Web Services Security: SOAP Message Security 1.0 (WS-Security (March 2004), At
  23. [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)CrossRefzbMATHGoogle Scholar
  24. [S+04] Schlimmer, J., et al.: A Proposal for UPnP 2.0 Device Architecture (May 2004), At
  25. [SMWC03] Shewchuk, J., Millet, S., Wilson, H., Cole, D.: Expanding the communications capabilities of web services with WSAddressing (2003), At
  26. [SS02] Scambay, J., Shema, M.: Hacking Web Applications Exposed. McGraw-Hill/Osborne, New York (2002)Google Scholar
  27. [Vog03] Vogels, W.: Web services are not distributed objects. IEEE Internet Computing 7(6), 59–66 (2003)CrossRefGoogle Scholar
  28. [W3C03] W3C. SOAP Version 1.2, W3C Recommendation (2003), at
  29. [Win98] Winer, D.: RPC over HTTP via XML (1998), At
  30. [Win99] Winer, D.: Dave’s history of SOAP (1999), At$555
  31. [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)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Karthikeyan Bhargavan
    • 1
  • Cédric Fournet
    • 1
  • Andrew D. Gordon
    • 1
  • Riccardo Pucella
    • 1
  1. 1.Microsoft ResearchUK

Personalised recommendations