Continuous Verification for Cryptographic Protocol Development

ABSTRACT

The proliferation of connected devices has motivated a surge in the development of cryptographic protocols to support a diversity of devices and use cases. To address this trend, we propose continuous verification, a methodology for secure cryptographic protocol design that consists of three principles: (1) repeated use of verification tools; (2) judicious use of common message components; and (3) inclusion of verifiable model specifications in standards. Our recommendations are derived from previous work in the formal methods community, as well as from our past experiences applying verification tools to improve standards. Through a case study of IETF protocols for the IoT, we illustrate the power of continuous verification by (i) discovering flaws in the protocols using the Cryptographic Protocol Shapes Analyzer (CPSA); (ii) identifying the corresponding fixes based on the feedback provided by CPSA; and (iii) demonstrating that verifiable models can be intuitive, concise and suitable for inclusion in standards to enable third-party verification and future modifications.

References

1. 2017. About | IoTivity. (2017). https://www.iotivity.org/about
2. Omar Almousa, Sebastian Mödersheim, and Luca Viganò. 2015. Alice and Bob: Reconciling Formal Models and Implementation. In Programming Languages with Applications to Biology and Security - Essays Dedicated to Pierpaolo Degano on the Occasion of His 65th Birthday. 66--85.
3. David Basin, Jannik Dreier, and Ralf Sasse. 2015. Automated symbolic proofs of observational equivalence. In Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. ACM, 1144--1155.
4. David A. Basin and Cas Cremers. 2014. Know Your Enemy: Compromising Adversaries in Protocol Analysis. ACM Trans. Inf. Syst. Secur. 17, 2 (2014), 7:1--7:31.
5. David A. Basin, Cas Cremers, and Simon Meier. 2013. Provably repairing the ISO/IEC 9798 standard for entity authentication. Journal of Computer Security 21, 6 (2013), 817--846.
6. Joachim Bauernberger. 2016. An incomplete List of Organizations and Alliances for the Internet of Things. (March 2016). https://www.linkedin.com/pulse/incomplete-list-organizations-alliances-internet-joachim-bauernberger
7. Bruno Blanchet. 2014. Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif. In Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures, Alessandro Aldini, Javier Lopez, and Fabio Martinelli (Eds.). Lecture Notes in Computer Science, Vol. 8604. Springer, 54--87.
8. Bluetooth. 2017. Volunteer With The Sig | Bluetooth Technology Website. (2017). https://www.bluetooth.com/membership-working-groups/volunteer-with-the-sig
9. Jonathan Bowen and Victoria Stavridou. 1993. Safety-critical systems, formal methods and standards. Software Engineering Journal 8, 4 (1993), 189--209.
10. Iliano Cervesato, Aaron D. Jaggard, Andre Scedrov, Joe-Kai Tsay, and Christopher Walstad. 2008. Breaking and fixing public-key Kerberos. Inf. Comput. 206, 2--4 (2008), 402--424.
11. Cas Cremers. 2011. Key exchange in IPsec revisited: Formal analysis of IKEv1 and IKEv2. In Computer Security--ESORICS 2011. Springer.
12. Cas Cremers and Sjouke Mauw. 2012. Operational semantics and verification of security protocols. Springer Science & Business Media.
13. Anupam Datta, Ante Derek, John C. Mitchell, and Dusko Pavlovic. 2004. Abstraction and Refinement in Protocol Derivation. In 17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004), 28-30 June 2004, Pacific Grove, CA, USA. 30.
14. Santiago Escobar, Catherine Meadows, and José Meseguer. 2009. Maude-NPA: Cryptographic protocol analysis modulo equational properties. In Foundations of Security Analysis and Design V. Springer, 1--50.
15. THAYER Fábrega, F Javier, Jonathan C Herzog, and Joshua D Guttman. 1999. Strand spaces: Proving security protocols correct. Journal of computer security 7, 2--3 (1999), 191--230.
16. Stefanie Gerdes, Ludwig Seitz, Goran Selander, Mehdi Mani, and Sandeep Kumar. 2016. Use Cases for Authentication and Authorization in Constrained Environments. RFC RFC7744. IETF.
17. Thomas Groß and Sebastian Mödersheim. 2011. Vertical Protocol Composition. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011. 235--250.
18. Joshua D. Guttman. 2014. Establishing and preserving protocol security goals. Journal of Computer Security 22, 2 (2014), 203--267.
19. Joshua D. Guttman, John D. Ramsdell, and Paul D. Rowe. 2016. Cross-Tool Semantics for Protocol Security Goals. Springer, 32--61. https://doi.org/10.1007/978-3-319-49100-4_2
20. Joshua D. Guttman and F. Javier Thayer. 2000. Protocol Independence through Disjoint Encryption. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, CSFW '00, Cambridge, England, UK, July 3-5, 2000. 24--34.
21. Anthony Hall. 1990. Seven myths of formal methods. IEEE software 7, 5 (1990), 11--19.
22. T Hardjono and N Smith. 2016. Fluffy: Simplified Key Exchange for Constrained Environments. Technical Report hardjono-ace-fluffy-03. https://datatracker.ietf.org/doc/rfc7744/
23. Thomas Hardjono and Brian Weis. 2004. The multicast group security architecture. RFC RFC 3740. IETF.
24. Paul Hoffman and Susan Harris. 2006. The Tao of IETF-A Novice's Guide to the Internet Engineering Task Force. Technical Report.
25. Mei Lin Hui and Gavin Lowe. 2001. Fault-Preserving Simplifying Transformations for Security Protocols. Journal of Computer Security 9, 1/2 (2001), 3--46.
26. ISO/IEC 2011. 29128: Information Technology - Security techniques --- Verification of Cryptographic Protocols. ISO/IEC.
27. Karen Rose, Scott Eldridge, and Lyman Chapin. 2017. The Internet of Things: An Overview, Understanding the Issues and Challenges of a More Connected World. Technical Report. Internet Society. https://www.internetsociety.org/sites/default/files/ISOC-IoT-Overview-20151221-en.pdf
28. John Kelsey, Bruce Schneier, and David A. Wagner. 1997. Protocol Interactions and the Chosen Protocol Attack. In Security Protocols, 5th International Workshop, Paris, France, April 7-9, 1997, Proceedings. 91--104.
29. Nadim Kobeissi, Karthikeyan Bhargavan, and Bruno Blanchet. 2017. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In IEEE European Symposium on Security and Privacy (EuroS&P).
30. Shin'ichiro Matsuo, Kunihiko Miyazaki, Akira Otsuka, and David A. Basin. 2010. How to Evaluate the Security of Real-Life Cryptographic Protocols? - The Cases of ISO/IEC 29128 and CRYPTREC. In Financial Cryptography and Data Security, FC 2010 Workshops, RLCPS, WECSR, and WLC 2010, Tenerife, Canary Islands, Spain, January 25-28, 2010, Revised Selected Papers. 182--194.
31. Catherine Meadows. 1999. Analysis of the Internet Key Exchange Protocol using the NRL Protocol Analyzer. In Proceedings, 1999 IEEE Symposium on Security and Privacy. IEEE CS Press.
32. Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN prover for the symbolic analysis of security protocols. In International Conference on Computer Aided Verification. Springer, 696--701.
33. MITRE. 2017. cpsa: Cryptographic Protocol Shapes Analyzer. (July 2017). https://github.com/mitre/cpsa
34. C Neuman, T Yu, S Hartman, and K Raeburn. 2005. The Kerberos network authentication service (V5). Standards Track RFC4120. https://www.ietf.org/rfc/rfc4120.txt
35. OCF. 2017. Open Connectivity Foundation (OCF). (2017). https://openconnectivity.org/
36. Kenneth G. Paterson and Thyla van der Merwe. 2016. Reactive and Proactive Standardisation of TLS. In Security Standardisation Research - Third International Conference, SSR 2016, Gaithersburg, MD, USA, December 5-6, 2016, Proceedings. 160--186.
37. John D Ramsdell, Joshua D Guttman, Moses D Liskov, and Paul D Rowe. 2009. The CPSA Specification: A Reduction System for Searching for Shapes in Cryptographic Protocols. The MITRE Corporation (2009).
38. Lukas Reinfurt, Uwe Breitenbücher, Michael Falkenthal, Frank Leymann, and Andreas Riegg. 2016. Internet of Things Patterns. In Proceedings of the 21st European Conference on Pattern Languages of Programs (EuroPlop '16). ACM, New York, NY, USA, 5:1--5:21. https://doi.org/10.1145/3011784.3011789
39. Paul D. Rowe, Joshua D. Guttman, and Moses D. Liskov. 2016. Measuring protocol strength with security goals. Int. J. Inf. Sec. 15, 6 (2016), 575--596.
40. Tara Salman and Raj Jain. 2015. Networking Protocols and Standards for Internet of Things. Internet of Things and Data Analytics Handbook (2015), 215--238.
41. Jerome H Saltzer and M Frans Kaashoek. 2009. Principles of computer system design: an introduction. Morgan Kaufmann.
42. Christoph Sprenger and David A. Basin. 2010. Developing security protocols by refinement. In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010. 361--374.
43. David J. Wu, Ankur Taly, Asim Shankar, and Dan Boneh. 2016. Privacy, Discovery, and Authentication for the Internet of Things. arXiv:1604.06959 [cs] (April 2016). http://arxiv.org/abs/1604.06959 arXiv: 1604.06959.
44. Z-Wave. 2017. - The Internet of Things is powered by Z-Wave. (2017). http://z-wavealliance.org/
45. Zigbee. 2017. zigbee alliance. (2017). http://www.zigbee.org/

Index Terms

• Security and privacy

  • Network security

    • Security protocols