Generating formal cryptographic protocol specifications
Ulf Carlsen · 2002
This paper describes a tool which translates a cryptographic protocol specified in the semi-formal standard notation i. A/spl rarr/B:M into the formal language CKT5. We examine the standard notation syntax, and describe how it is exploited by the tool to infer protocol conditions which must hold for every principal, thereby obtaining a complete, formal specification of the protocol. The translation criteria described herein are applicable to other target languages than CKT5.>