A semantics for web services authentication. (English) Zbl 1142.68587
Summary: We consider the problem of specifying and verifying cryptographic security protocols for XML web services. The security specification WS-Security describes a range of XML security elements, such as username tokens, public-key certificates, and digital signatures, amounting to a flexible vocabulary for expressing protocols. To describe the syntax of these elements, we extend the usual XML data model with symbolic representations of cryptographic values. We use predicates on this data model to describe the semantics of security elements and of sample protocols distributed with the Microsoft WSE implementation of WS-Security. By embedding our data model within Abadi and Fournet’s applied pi calculus, we formulate and prove security properties with respect to the standard Dolev-Yao threat model. Moreover, we informally discuss issues not addressed by the formal model. To the best of our knowledge, this is the first approach to the specification and verification of security protocols based on a faithful account of the XML wire format.
MSC:
| 68U35 | Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) |
| 68M10 | Network design and communication in computer systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 94A62 | Authentication, digital signatures and secret sharing |
References:
| [1] | M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: 28th ACM Symp. on Principles of Programming Languages (POPL’01), 2001, pp. 104-115.; M. Abadi, C. Fournet, Mobile values, new names, and secure communication, in: 28th ACM Symp. on Principles of Programming Languages (POPL’01), 2001, pp. 104-115. · Zbl 1323.68398 |
| [2] | M. Abadi, C. Fournet, Private authentication, Theoret. Comput. Sci. 322 (3) (2004) 427-476.; M. Abadi, C. Fournet, Private authentication, Theoret. Comput. Sci. 322 (3) (2004) 427-476. · Zbl 1071.68006 |
| [3] | M. Abadi, C. Fournet, G. Gonthier, Authentication primitives and their compilation, in: 27th ACM Symp. on Principles of Programming Languages (POPL’00), 2000, pp. 302-315.; M. Abadi, C. Fournet, G. Gonthier, Authentication primitives and their compilation, in: 27th ACM Symp. on Principles of Programming Languages (POPL’00), 2000, pp. 302-315. · Zbl 1323.68178 |
| [4] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press: Cambridge University Press Cambridge |
| [5] | K. Bhargavan, C. Fournet, A.D. Gordon, A semantics for web services authentication, in: 31st ACM Symp. on Principles of Programming Languages (POPL’04), 2004, pp. 198-209.; K. Bhargavan, C. Fournet, A.D. Gordon, A semantics for web services authentication, in: 31st ACM Symp. on Principles of Programming Languages (POPL’04), 2004, pp. 198-209. · Zbl 1325.68140 |
| [6] | K. Bhargavan, C. Fournet, A.D. Gordon, A semantics for web services authentication, Technical Report MSR-TR-2003-83, Microsoft Research, 2004.; K. Bhargavan, C. Fournet, A.D. Gordon, A semantics for web services authentication, Technical Report MSR-TR-2003-83, Microsoft Research, 2004. · Zbl 1325.68140 |
| [7] | K. Bhargavan, C. Fournet, A.D. Gordon, R. Pucella, TulaFale: a security tool for web services, in: Formal Methods for Components and Objects (FMCO’03), Lecture Notes in Computer Science, vol. 3188, Springer, Berlin, 2004.; K. Bhargavan, C. Fournet, A.D. Gordon, R. Pucella, TulaFale: a security tool for web services, in: Formal Methods for Components and Objects (FMCO’03), Lecture Notes in Computer Science, vol. 3188, Springer, Berlin, 2004. · Zbl 1104.68306 |
| [8] | B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: 14th IEEE Comput. Security Found. Workshop (CSFW-14), IEEE Computer Society, Silver Spring, MD, 2001, pp. 82-96.; B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: 14th IEEE Comput. Security Found. Workshop (CSFW-14), IEEE Computer Society, Silver Spring, MD, 2001, pp. 82-96. |
| [9] | D. Box, D. Ehnebuske, G. Kakivaya, A. Layman, N. Mendelsohn, H. Nielsen, S. Thatte, D. Winer, Simple Object Access Protocol (SOAP) 1.1, 2000, W3C Note, at; D. Box, D. Ehnebuske, G. Kakivaya, A. Layman, N. Mendelsohn, H. Nielsen, S. Thatte, D. Winer, Simple Object Access Protocol (SOAP) 1.1, 2000, W3C Note, at |
| [10] | J. Boyer, Canonical XML, 2001, W3C Recommendation, at; J. Boyer, Canonical XML, 2001, W3C Recommendation, at |
| [11] | J. Boyer, D.E. Eastlake, J. Reagle, Exclusive XML Canonicalization, 2002. W3C Recommendation, at; J. Boyer, D.E. Eastlake, J. Reagle, Exclusive XML Canonicalization, 2002. W3C Recommendation, at |
| [12] | Burrows, M.; Abadi, M.; Needham, R. M., A logic of authentication, Proc. Roy. Soc. London A, 426, 233-271 (1989) · Zbl 0687.68007 |
| [13] | E. Cohen, TAPS: a first-order verifier for cryptographic protocols, in: 13th IEEE Comput. Security Found. Workshop; IEEE Computer Society Press, Silver Spring, MD, 2000, pp. 144-158.; E. Cohen, TAPS: a first-order verifier for cryptographic protocols, in: 13th IEEE Comput. Security Found. Workshop; IEEE Computer Society Press, Silver Spring, MD, 2000, pp. 144-158. |
| [14] | J. Cowan, R. Tobin, XML Information Set, 2001, W3C Recommendation, at; J. Cowan, R. Tobin, XML Information Set, 2001, W3C Recommendation, at |
| [15] | Damiani, E.; De Capitani di Vimercati, S.; Paraboschi, S.; Samarati, P., Securing SOAP e-services, Internat. J. Inform. Security, 1, 2, 100-115 (2002) · Zbl 1060.68592 |
| [16] | E. Damiani, S. De Capitani di Vimercati, P. Samarati, Towards securing XML web services, in: ACM Workshop on XML Security 2002, 2003, pp. 90-96.; E. Damiani, S. De Capitani di Vimercati, P. Samarati, Towards securing XML web services, in: ACM Workshop on XML Security 2002, 2003, pp. 90-96. · Zbl 1060.68592 |
| [17] | T. Dierks, C. Allen, The TLS protocol: Version 1.0, 1999, RFC 2246.; T. Dierks, C. Allen, The TLS protocol: Version 1.0, 1999, RFC 2246. |
| [18] | Dolev, D.; Yao, A. C., On the security of public key protocols, IEEE Trans. Inform. Theory, IT-29, 2, 198-208 (1983) · Zbl 0502.94005 |
| [19] | D. Eastlake, P. Jones, US Secure Hash Algorithm 1 (SHA1), 2001, RFC 3174.; D. Eastlake, P. Jones, US Secure Hash Algorithm 1 (SHA1), 2001, RFC 3174. |
| [20] | D. Eastlake, J. Reagle, D. Solo, M. Bartel, J. Boyer, B. Fox, B. LaMacchia, E. Simon, XML-Signature Syntax and Processing, 2002, W3C Recommendation, at; D. Eastlake, J. Reagle, D. Solo, M. Bartel, J. Boyer, B. Fox, B. LaMacchia, E. Simon, XML-Signature Syntax and Processing, 2002, W3C Recommendation, at |
| [21] | Focardi, R.; Gorrieri, R.; Martinelli, F., A comparison of three authentication properties, Theoret. Comput. Sci., 291, 3, 285-327 (2003) · Zbl 1052.68033 |
| [22] | Gordon, A. D.; Jeffrey, A., Authenticity by typing for security protocols, J. Comput. Security, 11, 4, 451-521 (2003) |
| [23] | A.D. Gordon, R. Pucella, Validating a web service security abstraction by typing, in: ACM Workshop on XML Security 2002, 2003, pp. 18-29.; A.D. Gordon, R. Pucella, Validating a web service security abstraction by typing, in: ACM Workshop on XML Security 2002, 2003, pp. 18-29. · Zbl 1080.68523 |
| [24] | J. Jonsson, B. Kaliski, Public-Key Cryptography Standards (PKCS) #1: RSA Cryptography Specifications Version 2.1, 2003, RFC 3447.; J. Jonsson, B. Kaliski, Public-Key Cryptography Standards (PKCS) #1: RSA Cryptography Specifications Version 2.1, 2003, RFC 3447. |
| [25] | Kemmerer, R.; Meadows, C.; Millen, J., Three systems for cryptographic protocol analysis, J. Cryptol., 7, 2, 79-130 (1994) · Zbl 0814.94011 |
| [26] | H. Krawczyk, M. Bellare, R. Canetti, HMAC: keyed-hashing for message authentication, 1997, RFC 2104.; H. Krawczyk, M. Bellare, R. Canetti, HMAC: keyed-hashing for message authentication, 1997, RFC 2104. |
| [27] | G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, 1996, pp. 147-166.; G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR, in: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Vol. 1055, Springer, Berlin, 1996, pp. 147-166. |
| [28] | G. Lowe, A hierarchy of authentication specifications, in: Proc. 10th IEEE Comput. Security Found. Workshop, 1997, IEEE Computer Society Press, Silver Spring, MD, 1997, pp. 31-44.; G. Lowe, A hierarchy of authentication specifications, in: Proc. 10th IEEE Comput. Security Found. Workshop, 1997, IEEE Computer Society Press, Silver Spring, MD, 1997, pp. 31-44. |
| [29] | Microsoft Corporation, Microsoft .NET Pet Shop, 2002, at; Microsoft Corporation, Microsoft .NET Pet Shop, 2002, at |
| [30] | Microsoft Corporation, Web Services Enhancements for Microsoft .NET, December 2002, at; Microsoft Corporation, Web Services Enhancements for Microsoft .NET, December 2002, at |
| [31] | Milner, R., Communicating and Mobile Systems: the \(\pi \)-Calculus (1999), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0942.68002 |
| [32] | A. Nadalin, C. Kaler, P. Hallam-Baker, R. Monzillo, OASIS Web Services Security: SOAP Message Security 1.0 (WS-Security 2004), March 2004, at; A. Nadalin, C. Kaler, P. Hallam-Baker, R. Monzillo, OASIS Web Services Security: SOAP Message Security 1.0 (WS-Security 2004), March 2004, at |
| [33] | Needham, R. M.; Schroeder, M. D., Using encryption for authentication in large networks of computers, Comm. Assoc. Comput. Mach., 21, 12, 993-999 (1978) · Zbl 0387.68003 |
| [34] | H.F. Nielsen, S. Thatte, Web services routing protocol (WS-Routing), at; H.F. Nielsen, S. Thatte, Web services routing protocol (WS-Routing), at |
| [35] | Paulson, L. C., The inductive approach to verifying cryptographic protocols, J. Comput. Security, 6, 85-128 (1998) |
| [36] | Saltzer, J. H.; Reed, D. P.; Clark, D. D., End-to-end arguments in system design, ACM Trans. Comput. Systems, 2, 4, 277-288 (1984) |
| [37] | Satyanarayanan, M., Integrating security in a large distributed system, ACM Trans. Comput. Systems, 7, 3, 247-280 (1989) |
| [38] | J. Siméon, P. Wadler, The essence of XML, in: 30th ACM Symp. on Principles of Programming Languages (POPL’03), 2003, pp. 1-13.; J. Siméon, P. Wadler, The essence of XML, in: 30th ACM Symp. on Principles of Programming Languages (POPL’03), 2003, pp. 1-13. |
| [39] | Thayer Fábrega, F. J.; Herzog, J. C.; Guttman, J. D., Strand spaces: proving security protocols correct, J. Comput. Security, 7, 191-230 (1999) |
| [40] | L. van Doorn, M. Abadi, M. Burrows, E. Wobber, Secure network objects, in: IEEE Comput. Soc. Symp. on Research in Security and Privacy, 1996, pp. 211-221.; L. van Doorn, M. Abadi, M. Burrows, E. Wobber, Secure network objects, in: IEEE Comput. Soc. Symp. on Research in Security and Privacy, 1996, pp. 211-221. |
| [41] | Vogels, W., Web services are not distributed objects, IEEE Internet Comput., 7, 6, 59-66 (2003) |
| [42] | T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Comput. Soc. Symp. on Research in Security and Privacy, 1993, pp. 178-194.; T.Y.C. Woo, S.S. Lam, A semantic model for authentication protocols, in: IEEE Comput. Soc. Symp. on Research in Security and Privacy, 1993, pp. 178-194. |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
