暗号プロトコル記述からカラーペトリネットへの変換による機密性検証  [in Japanese] Secrecy Verification by Transforming Cryptographic Protocol Descriptions to Coloured Petri Nets  [in Japanese]

Search this Article

Author(s)

Abstract

カラーペトリネット(CPN)の可達性判定は決定可能であるので, 暗号プロトコルの安全性をカラーペトリネットの可達性判定に帰着することにより, 機械的な安全性検証が可能である.本稿では, プロトコル記述言語によって記述された暗号プロトコルをCPNに変換するアルゴリズムを提案し, 安全性の一つである機密性が, 変換によって得られるCPNの可達性判定問題に帰着させて検証できることを示す.

Verification of the safety of cryptographic protocols can be mechanized by reducing the safety to the reachability of Coloured Petri Nets (CPNs) since the reachability of CPNs is known to be decidable. In this paper, we propose an algorithm that transforms cryptographic protocol descriptions to CPNs, and show that the protocol is secure if no critical states are reachable from the initial states in the CPN obtained by the transformation from a given cryptographic protocol.

Journal

  • IEICE technical report

    IEICE technical report 105(490), 19-24, 2005-12-19

    The Institute of Electronics, Information and Communication Engineers

References:  5

Codes

  • NII Article ID (NAID)
    110003488391
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    7768647
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top