ITR: Cryptographic Protocol Transformations

Sri International, Menlo Park CA

Investigators

Abstract

One of the most theoretically challenging and practically important problems in modern computer science is the analysis of cryptographic authentication protocols, which play an essential role in Internet privacy and security. There is a general cryptographic protocol specification environment developed at SRI that includes a high-level specification language, CAPSL, and an intermediate language, CIL, based on a multiset rewriting rule model. The objective of this project is to write a translator to generate prototype protocol implementations in Java from CAPSL specifications. The translator will use existing Java classes and APIs (application program interfaces) for communication and encryption tasks. Concrete interface routines will be generated from the CIL representation. The advantage of this approach is that the originally specified protocol can be shown to be free of design flaws through analysis of the CIL using other tools.