Abstract:
The use of cryptographic protocols that enforce a variety of security properties has become more and more important in every day’s Internet transactions. The task of designing such protocols is tedious and error prone: many protocols that were believed to be correct for years have been shown to contain subtle errors. Moreover, it is difficult to design protocols that are adaptable to different constraints on their execution environment such as CPU power and bandwith. Security protocols can be built from simple communication primitives provided by standard protocols, and from cryptographic primitives. The rules of the protocol, can be derived from a high-level specification of what the protocol is designed to achieve, and under what hardware and software constraints it will be used. It has been shown that most of these specifications are best captured from a knowledge and belief-based viewpoint. In this work, we propose a technique allowing the automatic synthesis of security protocols that satisfy, by construction, their logical specification. Such specifications can be expressed using high-level communication primitives. Primitives have security and cryptographic attributes that include confidentiality, integrity, authentication, and nonrepudiation, and can be implemented using public and secret cryptography.