項正規表現に基づく Spi 計算の機密性検証  [in Japanese] Secrecy Verification of Spi Calculus based on Term Regular Expressions  [in Japanese]

Search this Article

Author(s)

Abstract

π計算に暗号化機能を加えた並行計算モデルであるspi計算を用いることにより,機密性の定式化とその検証が可能である.これまでに,spi計算に基づいた機密性検証の発見的手法は示されているが,自動検証手法の開発が望まれる.本稿では,spi計算の下で機密性の定式化を行い,プロセスが機密性を守る十分条件を与えるとともに,項正規表現を用いた十分条件の判定手法を提案する.

By using spi calculus, which is an extension of π calculus with cryptographic primitives, we can formulate and verify secrecy of processes. It is desired to develop automatic methods for verifying secrecy of processes although there were several heuristic methods studied so far. In this paper, for the automation of secrecy verifications in spi calculus, we first formulate secrecy of processes and give a sufficient condition for the secrecy. We then propose a method for deciding the sufficient condition based on term regular expressions.

Journal

  • IEICE technical report

    IEICE technical report 105(596), 35-40, 2006-02-02

    The Institute of Electronics, Information and Communication Engineers

References:  5

Codes

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