Subject: [Ietf-hub-boston] Papers related to Continuous Verification for Cryptographic Protocol Development

From: "Molina-Markham, Andres D." <[email-masked]>
Date: Thu, 26 Oct 2017 13:34:30 +0000

All,

It was great meeting you at The Burren, during October’s IETF-HUB meeting.

As a follow up, I am including a few of the most relevant papers about cryptographic protocol verification using our tool Cryptographic Protocol Shapes Analyzer (CPSA) [1- 3].

Please reach out if you are interested in learning more about our verification tool (available at https://github.com/mitre/cpsa).

I am looking forward to seeing you during the next HUB meeting.

Cheers,
Andres

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] A. Molina-Markham and P. D. Rowe. Continuous Verification for Cryptographic Protocol Development. Forthcoming ACM Workshop on the Internet of Safe Things, 2017.
[2] Joshua D. Guttman. Shapes: Surveying Crypto Protocol Runs. Invited chapter in Formal Models and Techniques for Analyzing Security Protocols, ed. Véronique Cortier and Steve Kremer. IOS Press, 2011, Cryptology and Information Security Series. Available from http://web.cs.wpi.edu/~guttman/pubs/shapes_surveying.pdf
[3] Joshua D. Guttman and Moses D. Liskov and Paul D. Rowe. Measuring Protocol Strength with Security Goals. International Journal of Information Security. DOI 10.1007/s10207-016-0319-z, February 2016. Springer Link to view-anywhere version: http://rdcu.be/mF3G.