SPINACH

 

Security protocols are a crucial building block of modern networks and distributed applications. Many methods exist to analyze protocols, but very few methods exist to design or construct secure protocols.

Our objective is to provide a methodology for the incremental construction of security protocols whose correctness (security) follows by design. To achieve this, we will develop a family of security-strengthening transformations, which take security protocols and transform them in such a way that they satisfy strong, clearly specified security properties. To justify the correctness of the transformations, we will use a framework that we have recently developed for specifying and reasoning about security protocols with respect to different classes of adversaries. This framework is an excellent starting point in that it provides:

• a novel fine-grained view of security properties and their relative strengths,
  

• the possibility of constructing proofs that a transformation indeed strengthens the security of a protocol, and
  

• tool support enabling the automated analysis of a large class of protocols and transformations.

We will apply our methodology to develop a family of novel security-strengthening transformations and to verify existing transformations from the literature. Together, these will provide a methodology for designing correct security protocols.

Contact: Cas Cremers, Michèle Feltz, Marko Horvat