Verified interoperable implementations of security protocols

ABSTRACT

We present an architecture and tools for verifying implementations of security protocols. Our implementations can run with both concrete and symbolic implementations of cryptographic algorithms. The concrete implementation is for production and interoperability testing. The symbolic implementation is for debugging and formal verification. We develop our approach for protocols written in F#, a dialect of ML, and verify them by compilation to ProVerif, a resolution-based theorem prover for cryptographic protocols. We establish the correctness of this compilation scheme, and we illustrate our approach with protocols for Web Services security.

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: Martín Abadi , Andrew D. Gordon, A calculus for cryptographic protocols, Information and Computation, v.148 n.1, p.1-70, Jan. 10, 1999 [doi>10.1006/inco.1998.2740]
• 3: Abadi, M. and Rogaway, P. 2002. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptol. 15, 2, 103--127.
• 4: 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]
• 5: Apache Software Foundation 2006. Apache WSS4J. Apache Software Foundation. http://ws.apache.org/wss4j/.
• 6: Askarov, A. and Sabelfeld, A. 2005. Security-typed languages for implementation of cryptographic protocols: A case study. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS'05). Lecture Notes in Computer Science, vol. 3679. Springer, 197--221.
• 7: Michael Backes , Birgit Pfitzmann , Michael Waidner, A composable cryptographic library with nested operations, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA [doi>10.1145/948109.948140]
• 8: Gerard Berry , Gerard Boudol, The chemical abstract machine, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.81-94, December 1989, San Francisco, California, United States [doi>10.1145/96709.96717]
• 9: 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]
• 10: Karthikeyan Bhargavan , Cédric Fournet , Ricardo Corin , Eugen Zalinescu, Cryptographically verified implementations for TLS, Proceedings of the 15th ACM conference on Computer and communications security, October 27-31, 2008, Alexandria, Virginia, USA [doi>10.1145/1455770.1455828]
• 11: Karthikeyan Bhargavan , Cédric Fournet , Andrew D. Gordon, Verifying policy-based security for web services, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA [doi>10.1145/1030083.1030120]
• 12: 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]
• 13: Bhargavan, K., Fournet, C., and Gordon, A. D. 2006b. 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, 88--106.
• 14: Bhargavan, K., Fournet, C., Gordon, A. D., and Pucella, R. 2004a. 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, 197--222.
• 15: 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]
• 16: 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]
• 17: Bhargavan, K., Fournet, C., Gordon, A. D., and Tse, S. 2007a. Verified interoperable implementations of security protocols. In Software System Reliability and Security. IOS Press, 87--115.
• 18: Bhargavan, K., Fournet, C., Gordon, A. D., and Tse, S. 2007b. Verified interoperable implementations of security protocols. Tech. rep. MSR-TR-2006-46, Microsoft Research.
• 19: 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
• 20: Bruno Blanchet, Computationally Sound Mechanized Proofs of Correspondence Assertions, Proceedings of the 20th IEEE Computer Security Foundations Symposium, p.97-111, July 06-08, 2007 [doi>10.1109/CSF.2007.16]
• 21: 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]
• 22: Bruno Blanchet , Andreas Podelski, Verification of cryptographic protocols: tagging enforces termination, Theoretical Computer Science, v.333 n.1-2, p.67-90, 1 March 2005 [doi>10.1016/j.tcs.2004.10.018]
• 23: Bodei, C., Buchholtz, M., Degano, P., and Nielson, F. 2003. Automatic validation of protocol narration. In Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW'03). 126--140.
• 24: Dolev, D. and Yao, A. 1983. On the security of public key protocols. IEEE Trans. Inform. Theor. IT--29, 2, 198--208.
• 25: Eastlake, D., Reagle, J., Imamura, T., Dillaway, B., and Simon, E. 2002. XML Encryption Syntax and Processing. W3C. W3C Recommendation.
• 26: Eastlake, D., Reagle, J., Solo, D., Bartel, M., Boyer, J., Fox, B., LaMacchia, B., and Simon, E. 2002. XML-Signature Syntax and Processing. W3C. W3C Recommendation.
• 27: Fournet, C. and Gonthier, G. 2005. A hierarchy of equivalences for asynchronous calculi. J. Logic Algeb. Program. 63, 131--173.
• 28: Galois Connections. 2005. Cryptol Reference Manual. Galois Connections.
• 29: Pablo Giambiagi , Mads Dam, On the secure implementation of security protocols, Science of Computer Programming, v.50 n.1-3, p.73-99, March 2004 [doi>10.1016/j.scico.2004.01.002]
• 30: Andrew D. Gordon , Riccardo Pucella, Validating a Web service security abstraction by typing, Proceedings of the 2002 ACM workshop on XML security, November 22-22, 2002, Fairfax, VA [doi>10.1145/764792.764797]
• 31: Goubault-Larrecq, J. and Parrennes, F. 2005. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05). Lecture Notes in Computer Science, vol. 3385. Springer, 363--379.
• 32: Guttman, J. D., Herzog, J. C., Ramsdell, J. D., and Sniffen, B. T. 2005. Programming cryptographic protocols. In Proceedings of the Conference Trusted Global Computing (TGC'05). Lecture Notes in Computer Science, vol. 3705. Springer, 116--145.
• 33: IBM Corporation. 2006. IBM WebSphere Application Server. IBM Corporation. http://www.ibm.com/software/websphere/.
• 34: Kleiner, E. and Roscoe, A. W. 2004. Web services security: A preliminary study using Casper and FDR. In Proceedings of the Conference Automated Reasoning for Security Protocol Analysis (ARSPA 04).
• 35: Kleiner, E. and Roscoe, A. W. 2005. On the relationship between Web services security and traditional protocols. In Proceedings of the Conference Mathematical Foundations of Programming Semantics (MFPS).
• 36: 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).
• 37: Massimo Merro , Davide Sangiorgi, On Asynchrony in Name-Passing Calculi, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.856-867, July 13-17, 1998
• 38: Microsoft Corporation. 2004. Web Services Enhancements (WSE) 2.0. Microsoft Corporation. http://msdn.microsoft.com/webservices/building/wse/default.aspx.
• 39: Microsoft Corporation. 2005. F#. Microsoft Corporation. http://research.microsoft.com/fsharp/.
• 40: Microsoft Corporation. 2006. Windows Communication Foundation (WCF). Microsoft Corporation. http://wcf.netfx3.com/.
• 41: Microsoft Corporation. 2007. FS2PV: A Cryptographic-Protocol Verifier for F#. Microsoft Corporation. http://research.microsoft.com/projects/samoa/.
• 42: Milner, R. 1992. Functions as processes. Math. Struct. Comput. Sci. 2, 2, 119--141.
• 43: Robin Milner, Communicating and mobile systems: the &pgr;-calculus, Cambridge University Press, New York, NY, 1999
• 44: Muller, F. and Millen, J. 2001. Cryptographic protocol generation from CAPSL. Tech. rep. SRI-CSL-01-07, SRI.
• 45: 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]
• 46: OASIS 2004. Web Services Security: SOAP Message Security 1.0 (WS-Security 2004). OASIS Standard.
• 47: O'Shea, N. 2006. Elyjah: A security analyzer for Java implementations of communications protocols. Fourth year project report, Computer Science, Division of Informatics, University of Edinburgh.
• 48: Dave Otway , Owen Rees, Efficient and timely mutual authentication, ACM SIGOPS Operating Systems Review, v.21 n.1, p.8-10, Jan. 1987 [doi>10.1145/24592.24594]
• 49: 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
• 50: 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
• 51: Sumii, E. and Pierce, B. C. 2001. Logical relations for encryption. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01). 256--269.
• 52: Eijiro Sumii , Benjamin C. Pierce, A bisimulation for dynamic sealing, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.161-172, January 14-16, 2004, Venice, Italy
• 53: W3C 2003. SOAP Version 1.2. W3C. W3C Recommendation.
• 54: W3C 2004. Web Services Addressing (WS-Addressing). W3C. W3C Member Submission.
• 55: 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

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

  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:
Functional programming, Web services, XML security, pi calculus