Issue No. 08 - Aug. (1986 vol. 12)
This paper discusses an automated technique for protocol development and its application to the specification, verification, and semiautomatic implementation of an authentication protocol for computer networks. We first give an overview of the specification language, implementation method, and software tools used with this technique. The authentication protocol is described, along with an example of its operation. We then discuss the reachability analysis technique for the verification of some protocol properties, and describe protocol verification software that uses this technique. Finally we present the results of the mechanical verification of some properties of this protocol and a partial implementation generated automatically from the protocol specification.
Protocols, Automata, Encryption, Authentication, Formal specifications, Software tools, Reachability analysis, state transition, Authentication, automated development tools, communication protocols, encryption, formal description technique, formal modeling, key distribution protocols, protocol implementation, protocol specification, protocol verification
"Mechanical verification and automatic implementation of communication protocols," in IEEE Transactions on Software Engineering, vol. 12, no. , pp. 827-843, 1986.