Introducing CafeOBJ (5) : Verification of an Authentication Protocol

DOI
  • OGATA Kazuhiro
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • FUTATSUGI Kokichi
    Graduate School of Information Science, Japan Advanced Institute of Science and Technology (JAIST)
  • NAKAMURA Masaki
    School of Electrical and Computer Engineering, Kanazawa University

Bibliographic Information

Other Title
  • CafeOBJ入門(5) 認証プロトコルの検証

Search this article

Description

An example of verification of authentication protocols with CafeOBJ algebraic specification language is shown. The NSLPK authentication protocol is based on the public-key cryptosystem. Two principals can use the protocol to achieve the mutual authentication between them. The successful completion of the message exchanges specified by the protocol lets two principals share some information. The secrecy property is as follows: even when there exist malicious principals, the information is never leaked to any third parties. Described is the verification with proof score that the protocol satisfies the (nonce) secrecy property.

Journal

  • Computer Software

    Computer Software 26 (1), 71-83, 2009

    Japan Society for Software Science and Technology

Details 詳細情報について

  • CRID
    1390001204736502272
  • NII Article ID
    130004549136
  • DOI
    10.11309/jssst.26.1_71
  • ISSN
    02896540
  • Data Source
    • JaLC
    • CiNii Articles
  • Abstract License Flag
    Disallowed

Report a problem

Back to top