In our previous post, we talked about the role of IETF in shaping the future of the internet and the exciting IETF meeting Montreal will host this summer. One topic we consider important in this context is the design of cryptographic protocols with formal proofs. We believe that formal methods have an important role to play; they should be more systematically applied in standardization to prove important security properties.
One of the items we from Ericsson Research will work on during the IETF 102 is the Limited Usage of Remote Keys (LURK) protocol. Bearing in mind that formal validations are a prerequisite for high levels of security assurance, we design and develop LURK by relying on formal methods to prove security guarantees.
The article Verifying Real-World Security Protocols presented the use of formal security analyses during the Security Area Open meeting of the IETF 101. They are expected to work hand-in-hand with standardization in order to provide strong cryptographic guarantees over the published protocols. Although the approach is not integrated into the definition of protocols yet, we consider it adapted for a robust protocol design and development.
First, the formal methods the authors use – Proverif and Cryptoverif – are very frequently called upon in security protocol automatic verification. For example, the Ericsson Research blog post LTE security procedures described application of the same formal methods in the context of LTE security procedures. Second, their research work has been very well received by the security community, winning a Distinguished Paper award at the prestigious 2017 IEEE Symposium on Security and Privacy S&P (Oakland 2017).
We decided to apply these practices in the design of the LURK protocol. The purpose of LURK is to protect the security credentials of a security service by isolating the operations associated to these credentials into a specific cryptographic service. The cryptographic service provides an interface to the other components that constitute the security service. The challenge consists in defining interactions with the Cryptographic Service that prevent leakage of the cryptographic credentials and protect against adversaries that replay some interactions. LURK opens possibilities of performing cryptographic exchange across the domains. One such use case is enabling delegation of video sessions from one domain, such as a Content Delivery Network (CDN) to another domain such as an Internet Service Provider (ISP) hosted “caches”, where a CDN can securely store content but without sharing of keys (see Figure 1). Our current focus is to define such interfaces for TLS (Transport Layer Security) 1.2 and TLS 1.3 so that TLS can be deployed securely over untrusted infrastructure or across different administrative domains like for CDN.
The IETF Hackathon provides the perfect platform where protocol design (with lurk, lurk-tls12), implementations (among others pylurk, clurk, key server) and more advanced security analysis can be discussed involving researchers from academia. Such activities are an integral part of our research work and contribution to IETF 102.
Together with our academic partner – Dr. Ioana Boureanu, Assistant Professor, University of Surrey – our efforts are therefore to push standardization of LURK supported by a thorough formal analysis. We already have a first LURK formal specification in Proverif, which is regularly refined to reflect the latest LURK updates.
It is a fact that formal methods are usually proposed by and dealt with in research. They have attracted some attention from the IETF community, at least in the area of cryptographic protocols. However, we believe that formal methods deserve even more attention and, fortunately, there is hope: with its continuously growing presence in these meetings, the research community seems to have started bringing forward formal design, development and verification, at the IETF. Stay tuned for an update in this context after the Montreal IETF 102 meeting!
Acknowledgments: The authors would like to thank Eva Fogelström, Jamal Hadi Salim, Joel Halpern, Michael Cameron, Makan Pourzandi, Charles Eckel, Yosr Jarraya, Amine Boukhtouta, Frederic Fieau, Polo Garcia Jesus Alberto Sanjay Mishra, and Zaheduzzaman Sarker for their feedback.