skip to main content
article

Secure sessions for Web services

Published: 01 May 2007 Publication History

Abstract

We address the problem of securing sequences of SOAP messages exchanged between web services and their clients. The WS-Security standard defines basic mechanisms to secure SOAP traffic, one message at a time. For typical web services, however, using WS-Security independently for each message is rather inefficient; moreover, it is often important to secure the integrity of a whole session, as well as each message. To these ends, recent specifications provide further SOAP-level mechanisms. WS-SecureConversation defines security contexts, which can be used to secure sessions between two parties. WS-Trust specifies how security contexts are issued and obtained. We develop a semantics for the main mechanisms of WS-Trust and WS-SecureConversation, expressed as a library for TulaFale, a formal scripting language for security protocols. We model typical protocols relying on these mechanisms and automatically prove their main security properties. We also informally discuss some pitfalls and limitations of these specifications.

References

[1]
Abadi, M. and Fournet, C. 2001. Mobile values, new names, and secure communication. In 28th ACM Symposium on Principles of Programming Languages (POPL'01). 104--115.
[2]
Abadi, M. and Gordon, A. D. 1999. A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1--70.
[3]
Abadi, M. and Rogaway, P. 2002. Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology 15, 2, 103--127.
[4]
Abadi, M., Blanchet, B., and Fournet, C. 2004. Just fast keying in the pi calculus. In 13th European Symposium on Programming (ESOP'04). LNCS, vol. 2986. Springer, New York. 340--354.
[5]
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Heám, P.-C., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., and Vigneron, L. 2005. The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In 17th International Conference on Computer Aided Verification (CAV'05), K. Etessami and S. K. Rajamani, Eds. LNCS, vol. 3576. Springer, New York. Available at http://www.avispa-project.org/publications.html.
[6]
Backes, M., Pfitzmann, B., and Waidner, M. 2003. A composable cryptographic library with nested operations. In 10th ACM Conference on Computer and Communications Security (CCS'03). 220--230.
[7]
Backes, M., Mödersheim, S., Pfitzmann, B., and Viganò, L. 2006. Symbolic and cryptographic analysis of the secure WS-ReliableMessaging scenario. In Foundations of Software Science and Computation Structures (FOSSACS'06). 428--445.
[8]
Barbir, A., Goodner, M., Gudgin, M., Granqvist, H., Nadalin, A., et al. 2006. Web Services Secure Conversation Language (WS-SecureConversation) Oasis Committee Draft Version 0.1. At http://www.oasis-open.org/committees/download.php/20158/ws-secureconversation-1.3-spec-cd-01.pdf.
[9]
Bhargavan, K., Corin, R., Fournet, C., and Gordon, A. D. 2004a. Secure sessions for web services. In 2004 ACM Workshop on Secure Web Services (SWS'04). 56--66.
[10]
Bhargavan, K., Corin, R., Fournet, C., and Gordon, A. D. 2004d. Secure sessions for web services. Tech. Rep. MSR-TR-2004-114, Microsoft Research.
[11]
Bhargavan, K., Fournet, C., and Gordon, A. D. 2004c. Verifying policy-based security for web services. In 11th ACM Conference on Computer and Communications Security (CCS'04). 268--277.
[12]
Bhargavan, K., Fournet, C., Gordon, A. D., and Pucella, R. 2004d. TulaFale: A security tool for web services. In International Symposium on Formal Methods for Components and Objects (FMCO'03). LNCS, vol. 3188. Springer, New York. 197--222.
[13]
Bhargavan, K., Fournet, C., and Gordon, A. D. 2005. A semantics for web services authentication. Theor. Comput. Sci. 340, 1 (June), 102--153.
[14]
Bhargavan, K., Fournet, C., Gordon, A. D., and Tse, S. 2006. Verified interoperable implementations of security protocols. In 19th IEEE Computer Security Foundations Workshop (CSFW'06). 139--152.
[15]
Blanchet, B. 2001. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14). IEEE Computer Society, Washington, D.C. 82--96.
[16]
Blanchet, B. 2002. From secrecy to authenticity in security protocols. In 9th International Static Analysis Symposium (SAS'02). LNCS, vol. 2477. Springer, New York. 342--359.
[17]
Blanchet, B. 2006. A computationally sound mechanized prover for security protocols. In IEEE Symposium on Security and Privacy. 140--154.
[18]
Box, D., Curbera, F., et al. 2004. Web Services Addressing (WS-Addressing). At http://www.w3.org/Submission/2004/SUBM-ws-addressing-20040810/.
[19]
Burrows, M., Abadi, M., and Needham, R. 1989. A logic of authentication. Proceedings of the Royal Society of London A 426, 233--271.
[20]
Cohen, E. 2000. TAPS: A first-order verifier for cryptographic protocols. In 13th IEEE Computer Security Foundations Workshop. IEEE Computer Society Press, Washington, D.C. 144--158.
[21]
Damiani, E., De Capitani di Vimercati, S., Paraboschi, S., and Samarati, P. 2002. Securing SOAP e-services. International Journal of Information Security 1, 2, 100--115.
[22]
Davis, D., Ferris, C., Gajjala, V., Gavrylyuk, K., Gudgin, M., Kaler, C., Langworthy, D., Moroney, M., Nadalin, A., Roots, J., Storey, T., Vishwanath, T., and Walter, D. 2005. WS-ReliableMessaging Interop Workshop. At ftp://www6.software.ibm.com/software/developer/library/ws-rmseconscenar io.doc.
[23]
Diffie, W. and Hellman, M. 1976. New directions in cryptography. IEEE Transactions on Information Theory IT-22, 6 (Nov.), 644--654.
[24]
Dolev, D. and Yao, A. 1983. On the security of public key protocols. IEEE Transactions on Information Theory IT--29, 2, 198--208.
[25]
Durgin, N. A., Mitchell, J. C., and Pavlovic, D. 2003. A compositional logic for proving security properties of protocols. Journal of Computer Security 11, 4, 677--721.
[26]
Ferris, C., Langworthy, D., et al. 2004. Web Services Reliable Messaging Protocol (WS-ReliableMessaging). At http://msdn.microsoft.com/ws/2004/03/ws-reliablemessaging/.
[27]
Freier, A. O., Karlton, P., and Kocher, P. C. November 1996. The SSL protocol: Version 3.0. http://home.netscape.com/eng/ssl3/draft302.txt.
[28]
Gollmann, D. 2003. Authentication by correspondence. IEEE Journal on Selected Areas in Communications 21, 1, 88--95.
[29]
Gordon, A. D. and Pucella, R. 2005. Validating a web service security abstraction by typing. Formal Aspects of Computing 17, 277--318.
[30]
Gross, T. and Pfitzmann, B. 2004. Proving a WS-Federation Passive Requestor profile. In 2004 ACM Workshop on Secure Web Services (SWS). ACM Press, New York.
[31]
Gudgin, M. 2004. Using WS-Trust and WS-SecureConversation. MSDN. At http://msdn.microsoft.com/library/default.asp?url=/library/en-us/dnwebsrv/html/ws-trustandsecureconv.asp.
[32]
Gudgin, M., Nadalin, A., et al. 2005a. Web Services Secure Conversation Language (WS-SecureConversation) Version 1.2. At http://www.oasis-open.org/committees/download.php/17364/lists.oasis-open.orgarchivesws-sx200512zip00000.zip.
[33]
Gudgin, M., Nadalin, A., et al. 2005b. Web Services Trust Language (WS-Trust) Version 1.2. At http://www.oasis-open.org/committees/download.php/17364/lists.oasis-open.orgarchivesws-sx200512zip00000.zip.
[34]
Gudgin, M., Nadalin, A., et al. 2005c. Web Services Trust Language (WS-Trust) Version 1.2. At http://www.oasis-open.org/committees/download.php/20160/ws-trust-1.3-spec-cd-01.pdf.
[35]
Harkins, D. and Carrel, D. 1998. RFC 2409: The Internet Key Exchange (IKE). http://www.ietf.org/rfc/rfc2409.txt.
[36]
Hui, M. L. and Lowe, G. 2001. Fault-preserving simplifying transformations for security protocols. Journal of Computer Security 9, 1/2, 3--46.
[37]
Johnson, J. E., Langworthy, D. E., Lamport, L., and Vogt, F. H. 2004. Formal specification of a web services protocol. In 1st International Workshop on Web Services and Formal Methods (WS-FM 2004). University of Pisa.
[38]
Kaler, C., Nadalin, A., et al. 2003a. Web Services Federation Language (WS-Federation) Version 1.0. At http://msdn.microsoft.com/ws/2003/07/ws-federation/.
[39]
Kaler, C., Nadalin, A., et al. 2003b. WS-Federation: Passive Requestor Profile Version 1.0. At ftp://www6.software.ibm.com/software/developer/library/ws-fedpass.pdf.
[40]
Kaler, C., Nadalin, A., et al. 2004a. Web Services Secure Conversation Language (WS-SecureConversation) Version 1.1. At http://msdn.microsoft.com/ws/2004/04/ws-secure-conversation/.
[41]
Kaler, C., Nadalin, A., et al. 2004b. Web Services Trust Language (WS-Trust) Version 1.1. At http://msdn.microsoft.com/ws/2004/04/ws-trust/.
[42]
Kemmerer, R., Meadows, C., and Millen, J. 1994. Three systems for cryptographic protocol analysis. Journal of Cryptology 7, 2, 79--130.
[43]
Keyser, C. 2004. Source code for SCT tokens in a farm source code. http://blogs.msdn.com/chriskeyser/archive/2004/11/30/272678.aspx.
[44]
Kleiner, E. and Roscoe, A. W. 2004. Web services security: A preliminary study using Casper and FDR. In Automated Reasoning for Security Protocol Analysis (ARSPA'04).
[45]
Kleiner, E. and Roscoe, A. W. 2005. On the relationship between web services security and traditional protocols. In Mathematical Foundations of Programming Semantics (MFPS XXI).
[46]
Lowe, G. 1996. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1055. Springer, New York. 147--166.
[47]
Lowe, G. 1997. A hierarchy of authentication specifications. In Proceedings of 10th IEEE Computer Security Foundations Workshop, 1997. IEEE Computer Society Press, Washington, D.C. 31--44.
[48]
Microsoft Corporation 2004. Web Services Enhancements (WSE) 2.0 SP1. Microsoft Corporation. At http://msdn.microsoft.com/webservices/building/wse/default.aspx.
[49]
Milner, R. 1999. Communicating and Mobile Systems: the π-Calculus. Cambridge University Press, Cambridge.
[50]
Nadalin, A., Kaler, C., Hallam-Baker, P., and Monzillo, R. 2004. OASIS Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard 200401. At http://docs.oasis-open.org/wss/2004/01/oasis-200401-wss-soap-message-security-1.0.pdf.
[51]
Needham, R. and Schroeder, M. 1978. Using encryption for authentication in large networks of computers. Commun. ACM 21, 12, 993--999.
[52]
OASIS Security Services TC 2005. Security Assertion Markup Language FAQ. OASIS Security Services TC. At http://www.oasis-open.org/committees/security/faq.php.
[53]
Paulson, L. 1998. The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6, 85--128.
[54]
Paulson, L. C. 1999. Inductive analysis of the internet protocol TLS. ACM Trans. Inf. Syst. Secur. 2, 3, 332--351.
[55]
Ryan, P. Y. A., Schneider, S. A., Goldsmith, M. H., Lowe, G., and Roscoe, A. W. 2001. The Modeling and Analysis of Security Protocols: the CSP Approach. Pearson Education.
[56]
Thayer Fábrega, F., Herzog, J., and Guttman, J. 1999. Strand spaces: Proving security protocols correct. Journal of Computer Security 7, 191--230.
[57]
Vogels, W. 2003. Web services are not distributed objects. IEEE Internet Computing 7, 6, 59--66.
[58]
W3C 2003. SOAP Version 1.2. W3C. W3C Recommendation, at http://www.w3.org/TR/soap12.
[59]
Woo, T. and Lam, S. 1993. A semantic model for authentication protocols. In IEEE Computer Society Symposium on Research in Security and Privacy. 178--194.
[60]
WS 2002. WS-Trust/WS-SecureConversation Interop Workshop. At http://msdn.microsoft.com/webservices/community/workshops/trustworkshop112003.aspx.
[61]
WS 2004. WS-SecureConversation/WS-Trust Interop Workshop. At http://msdn.microsoft.com/webservices/community/workshops/TrustWorkshop Oct2004.aspx.

Cited By

View all

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Information and System Security
ACM Transactions on Information and System Security  Volume 10, Issue 2
May 2007
144 pages
ISSN:1094-9224
EISSN:1557-7406
DOI:10.1145/1237500
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2007
Published in TISSEC Volume 10, Issue 2

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Web services
  2. XML security

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)7
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2019)Understanding Attestation: Analyzing Protocols that Use QuotesSecurity and Trust Management10.1007/978-3-030-31511-5_6(89-106)Online publication date: 26-Sep-2019
  • (2016)Trust Management and Delegation for the Administration of Web ServicesLeadership and Personnel Management10.4018/978-1-4666-9624-2.ch026(570-589)Online publication date: 2016
  • (2015)Security specification of WS-SecureConversation2015 IEEE Student Conference on Research and Development (SCOReD)10.1109/SCORED.2015.7449427(690-695)Online publication date: Dec-2015
  • (2015)Active Linking AttacksMathematical Foundations of Computer Science 201510.1007/978-3-662-48054-0_46(555-566)Online publication date: 11-Aug-2015
  • (2014)Trust Management and Delegation for the Administration of Web ServicesOrganizational, Legal, and Technological Dimensions of Information System Administration10.4018/978-1-4666-4526-4.ch002(18-37)Online publication date: 2014
  • (2013)Secure healthcare data sharing among federated health information systemsInternational Journal of Critical Computer-Based Systems10.1504/IJCCBS.2013.0590234:4(349-373)Online publication date: 1-Feb-2013
  • (2012)Interoperability and Functionality of WS-* ImplementationsInternational Journal of Web Services Research10.4018/jwsr.20120701019:3(1-22)Online publication date: 1-Jul-2012
  • (2012)Safe abstractions of data encodings in formal security protocol modelsFormal Aspects of Computing10.1007/s00165-012-0267-y26:1(125-167)Online publication date: 13-Nov-2012
  • (2011)Authentication and Authorization in Web ServicesNetworked Digital Technologies10.1007/978-3-642-22185-9_2(13-23)Online publication date: 2011
  • (2010)SecurityLarge-Scale Distributed Computing and Applications10.4018/978-1-61520-703-9.ch009(194-216)Online publication date: 2010
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media