Verifying policy-based web services security

ABSTRACT

WS-SecurityPolicy is a declarative language for configuring web services security mechanisms. We describe a formal semantics for WS-SecurityPolicy and propose a more abstract language for specifying secure links between web services and their clients. We present the architecture and implementation of tools that (1) compile policy files from link specifications, and (2) verify by invoking a theorem prover whether a set of policy files run by any number of senders and receivers correctly implements the goals of a link specification, in spite of active attackers. Policy-driven web services implementations are prone to the usual subtle vulnerabilities associated with cryptographic protocols; our tools help prevent such vulnerabilities. We can verify policies when first compiled from link specifications, and also re-verify policies against their original goals after any modifications during deployment. Moreover, we present general security theorems for all configurations that rely on compiled policies.

REFERENCES

• 1: Martín Abadi , Cédric Fournet, Mobile values, new names, and secure communication, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.104-115, January 2001, London, United Kingdom
• 2: Xavier Allamigeon , Bruno Blanchet, Reconstruction of Attacks against Cryptographic Protocols, Proceedings of the 18th IEEE workshop on Computer Security Foundations, p.140-154, June 20-22, 2005 [doi>10.1109/CSFW.2005.25]
• 3: Karthikeyan Bhargavan , Ricardo Corin , Cédric Fournet , Andrew D. Gordon, Secure sessions for Web services, ACM Transactions on Information and System Security (TISSEC), v.10 n.2, p.8-es, May 2007 [doi>10.1145/1237500.1237504]
• 4: Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon, A semantics for web services authentication, Theoretical Computer Science, v.340 n.1, p.102-153, 13 June 2005 [doi>10.1016/j.tcs.2005.03.005]
• 5: Bhargavan, K., Fournet, C., and Gordon, A. D. 2005b. Verifying policy-based security for web services. Tech. Rep. MSR--TR--2004--84, Microsoft Research. Nov.
• 6: Bhargavan, K., Fournet, C., and Gordon, A. D. 2006b. Policy advisor for WSE 3.0. In Web Service Security: Scenarios, patterns, and implementation guidance for Web Services Enhancements (WSE) 3.0. Microsoft Press, 324--330.
• 7: Bhargavan, K., Fournet, C., and Gordon, A. D. 2006c. Verified reference implementations of WS-Security protocols. In Proceedings of the 3rd International Workshop on Web Services and Formal Methods (WS-FM 2006). Lecture Notes in Computer Science, vol. 4184. Springer-Verlag, New York, 88--106.
• 8: Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon , Greg O'Shea, An advisor for web services security policies, Proceedings of the 2005 workshop on Secure web services, November 11-11, 2005, Fairfax, VA, USA [doi>10.1145/1103022.1103024]
• 9: Bhargavan, K., Fournet, C., Gordon, A. D., and Pucella, R. 2004. TulaFale: A security tool for web services. In Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO'03). Lecture Notes in Computer Science, vol. 3188. Springer-Verlag, New York, 197--222. Tool download available from http://Securing.WS.
• 10: Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon , Nikhil Swamy, Verified implementations of the information card federated identity-management protocol, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan [doi>10.1145/1368310.1368330]
• 11: Karthikeyan Bhargavan , Cedric Fournet , Andrew D. Gordon , Stephen Tse, Verified Interoperable Implementations of Security Protocols, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.139-152, July 05-07, 2006 [doi>10.1109/CSFW.2006.32]
• 12: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 13: Bruno Blanchet, From Secrecy to Authenticity in Security Protocols, Proceedings of the 9th International Symposium on Static Analysis, p.342-359, September 17-20, 2002
• 14: Bruno Blanchet , Cedric Fournet, Automated Verification of Selected Equivalences for Security Protocols, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.331-340, June 26-29, 2005 [doi>10.1109/LICS.2005.8]
• 15: Box, D., Christensen, E., Curbera, F., Ferguson, D., Frey, J., Hadley, M., Kaler, C., Langworthy, D., Leymann, F., Lovering, B., Lucco, S., Millet, S., Mukhi, N., Nottingham, M., Orchard, D., Shewchuk, J., Sindambiwe, E., Storey, T., Weerawarana, S., and Winkler, S. 2004. Web Services Addressing (WS-Addressing). W3C Submission.
• 16: Box, D., Curbera, F., Hondo, M., Kaler, C., Langworthy, D., Nadalin, A., Nagaratnam, N., Nottingham, M., von Riegen, C., and Shewchuk, J. 2003a. Web services policy framework (WS-Policy).
• 17: Box, D., Hondo, M., Kaler, C., Maruyama, H., Nadalin, A., Nagaratnam, N., Patrick, P., von Riegen, C., and Shewchuk, J. 2003b. Web services policy assertions language (WS-PolicyAssertions).
• 18: Della-Libera, G., Hallam-Baker, P., Hondo, M., Janczuk, T., Kaler, C., Maruyama, H., Nagaratnam, N., Nash, A., Philpott, R., Prafullchandra, H., Shewchuk, J., Waingold, E., and Zolfonoon, R. 2002. Web services security policy language (WS-SecurityPolicy). Version 1.0.
• 19: Dierks, T. and Rescorla, E. 2006. The Transport Layer Security (TLS) Protocol Version 1.1. RFC 4346, Internet Engineering Task Force Proposed Standard.
• 20: Dolev, D. and Yao, A. 1983. On the security of public key protocols. IEEE Trans. Inform. Theory IT--29, 2, 198--208.
• 21: Eastlake, D., Reagle, J., Imamura, T., Dillaway, B., and Simon, E. 2002a. XML Encryption Syntax and Processing. W3C Recommendation.
• 22: Eastlake, D., Reagle, J., Solo, D., Bartel, M., Boyer, J., Fox, B., LaMacchia, B., and Simon, E. 2002b. XML-Signature Syntax and Processing. W3C Recommendation.
• 23: Andrew D. Gordon , Alan Jeffrey, Authenticity by typing for security protocols, Journal of Computer Security, v.11 n.4, p.451-519, July 2003
• 24: Andrew D. Gordon , Riccardo Pucella, Validating a web service security abstraction by typing, Formal Aspects of Computing, v.17 n.3, p.277-318, October 2005 [doi>10.1007/s00165-004-0058-1]
• 25: Guttman, J. D. and Herzog, A. L. 2005. Rigorous automated network security management. Int. J. Inform. Secur. 4, 1--2, 29--48.
• 26: Lowe, G. 2002. Analyzing protocols subject to guessing attacks. In Proceedings of the Workshop on Issues in the Theory of Security (WITS'02). Portland, Oregon.
• 27: Lukell, S., Veldman, C., and Hutchison, A. C. M. 2003. Automated attack analysis and code generation in a multi-dimensional security protocol engineering framework. In Proceedings of the Southern African Telecommunication Networks and Applications Conference (SATNAC).
• 28: Microsoft Corporation 2004. Web Services Enhancements (WSE) 2.0. Microsoft Corporation.
• 29: Muller, F. and Millen, J. 2001. Cryptographic protocol generation from CAPSL. Tech. Rep. SRI--CSL--01--07, SRI.
• 30: Nadalin, A., Griffin, P., Kaler, C., Hallam-Baker, P., and Monzillo, R. 2004a. Web Services Security: UsernameToken Profile 1.0. OASIS Standard.
• 31: Nadalin, A., Kaler, C., Hallam-Baker, P., and Monzillo, R. 2004b. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard.
• 32: Nadalin, A., Kaler, C., Hallam-Baker, P., and Monzillo, R. 2006. Web Services Security: SOAP Message Security 1.1 (WS-Security 2004). OASIS Standard.
• 33: Nadalin, A., Goodner, M., Gudgin, M., Barbir, A., and Granqvist, H. 2007. WS-SecurityPolicy 1.2. OASIS Standard.
• 34: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 35: Dawn Xiaodong Song , Adrian Perrig , Doantam Phan, AGVI - Automatic Generation, Verification, and Implementation of Security Protocols, Proceedings of the 13th International Conference on Computer Aided Verification, p.241-245, July 18-22, 2001
• 36: Davide Pozza , Riccardo Sisto , Luca Durante, Spi2Java: Automatic Cryptographic Protocol Java Code Generation from spi calculus, Proceedings of the 18th International Conference on Advanced Information Networking and Applications, p.400, March 29-31, 2004
• 37: Michiaki Tatsubori , Takeshi Imamura , Yuhichi Nakamura, Best-Practice Patterns and Tool Support for Configuring Secure Web Services Messaging, Proceedings of the IEEE International Conference on Web Services, p.244, June 06-09, 2004 [doi>10.1109/ICWS.2004.30]
• 38: W3C. 1999. XML Path Language (XPath) Version 1.0. W3C. W3C Recommendation.
• 39: W3C. 2003. SOAP Version 1.2. W3C. W3C Recommendation.
• 40: Thomas Y. C. Woo , Simon S. Lam, A Semantic Model for Authentication Protocols, Proceedings of the 1993 IEEE Symposium on Security and Privacy, p.178, May 24-26, 1993
• 41: Lantian Zheng , Stephen Chong , Andrew C. Myers , Steve Zdancewic, Using Replication and Partitioning to Build Secure Distributed Systems, Proceedings of the 2003 IEEE Symposium on Security and Privacy, p.236, May 11-14, 2003

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
      F.3.2 Semantics of Programming Languages
      F.3.3 Studies of Program Constructs

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Languages, Security, Theory, Verification

Keywords:
Web services, XML security, pi calculus