Use of a formal description technique in the specification of authentication protocols

Vijay Varadharajan*

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


Formal specification techniques have been employed over the past decade or so by various workers in data communication and computer network systems in order to provide both definitional specifications of protocols and models of protocols for analytic purposes. This paper considers the use of the specification language LOTOS (Language of Temporal Ordering Specification) for specifying some authentication protocols developed in the security field. The language LOTOS recently became an International ISO Standard and the protocols specified form part of the ISO and CCITT Standards. In fact, the CCITT protocol which is considered in this paper, has been used in the LOCATOR (X.400 Secure Mail) project within HPLabs. We first give a brief introduction to LOTOS and then specify two security protocols from ISO/DP 9798 and CCITT X.509 Standards. We feel that a formal specification of protocols is a useful and a necessary step towards understandability, analysis and implementation of the protocols. Further, we feel that LOTOS possesses the necessary features required for specifying such protocols.

Original languageEnglish
Pages (from-to)203-215
Number of pages13
JournalComputer Standards and Interfaces
Issue number3
Publication statusPublished - 1989
Externally publishedYes


  • Authentication
  • CCITT X. 509
  • Computer network systems
  • Data communication
  • Formal specification
  • ISO/DP 9798
  • Modeling
  • Protocols
  • X.400


Dive into the research topics of 'Use of a formal description technique in the specification of authentication protocols'. Together they form a unique fingerprint.

Cite this