next up previous
Next: Introduction

A First Step towards the Automatic Generation of Security Protocols

Adrian Perrig
perrig@cs.berkeley.edu - Dawn Song
dawnsong@cs.berkeley.edu -
Computer Science Department
Carnegie Mellon University and University of California, Berkeley

Abstract:

This paper describes automatic protocol generation (APG for short), a novel mechanism to generate security protocols automatically. With APG, the protocol designer inputs the specification of the desired security properties and the system requirements. The system requirements include a metric function which specifies the cost or overhead of protocol primitives, which defines an ordering over protocols with respect to the metric function. Based on this ordering, APG explores the protocol space and outputs the correct protocol which has minimal cost with respect to the metric function, as well as satisfies the security properties and system requirements.

The APG approach has several advantages over the current protocol design process. It is fully automatic, and hence, more efficient than a manual process. The protocols generated by APG offer higher confidence, because they are verified by a powerful protocol analyzer. Another significant advantage is that, because APG search through the protocol space in the order of increasing cost with respect to the metric function, APG generates correct protocols with minimal cost which ideally suit the system requirements. Furthermore, APG is flexible in the sense that it can handle different security properties and different system requirements.

To gain experience with APG, we conduct a case study on the automatic generation of two-party, mutual authentication protocols. In one experiment, APG generates authentication protocols that are simpler than the standard protocols documented in the literature (i.e., ISO standards [Int93]). In another experiment, the automatic protocol generation generates different protocols with minimal cost for varying requirements, hence demonstrating its capability to produce high quality protocols.




next up previous
Next: Introduction

Adrian Perrig
Fri Sep 1 21:14:38 PDT 2000