Technical reports

Security protocol design by composition

Hyun-Jin Choi

January 2006, 155 pages

This technical report is based on a dissertation submitted December 2004 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Churchill College.

DOI: 10.48456/tr-657

Abstract

The aim of this research is to present a new methodology for the systematic design of compound protocols from their parts. Some security properties can be made accumulative, i.e. can be put together without interfering with one another, by carefully selecting the mechanisms which implement them. Among them are authentication, secrecy and non-repudiation. Based on this observation, a set of accumulative protocol mechanisms called protocol primitives are proposed and their correctness is verified. These protocol primitives are obtained from common mechanisms found in many security protocols such as challenge and response. They have been carefully designed not to interfere with each other. This feature makes them flexible building blocks in the proposed methodology. Equipped with these protocol primitives, a scheme for the systematic construction of a complicated protocol from simple protocol primitives is presented, namely, design by composition. This design scheme allows the combination of several simple protocol parts into a complicated protocol without destroying the security properties established by each independent part. In other words, the composition framework permits the specification of a complex protocol to be decomposed into the specifications of simpler components, and thus makes the design and verification of the protocol easier to handle. Benefits of this approach are similar to those gained when using a modular approach to software development.

The applicability and practicality of the proposed methodology are validated through many design examples of protocols found in many different environments and with various initial assumptions. The method is not aimed to cover all existent design issues, but a reasonable range of protocols is addressed.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-657,
  author =	 {Choi, Hyun-Jin},
  title = 	 {{Security protocol design by composition}},
  year = 	 2006,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-657.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-657},
  number = 	 {UCAM-CL-TR-657}
}