セキュリティプロトコルの略式記法からspi 計算への変換

• 住井英二郎

• 立沢, 秀晃

• 米澤, 明憲

書誌事項

タイトル別名

• セキュリティプロトコル ノ リャクシキ キホウ カラ spi ケイサン エ ノ ヘンカン
• Translating Security Protocols from Informal Notation into Spi Calculus

抄録

セキュリティプロトコルは往々にして非形式的な略式記法で定義されるが，この記法は明確な意味論がなく，プロトコルが正常に完了する場合のメッセージ列しか記述していない．そのためにプロトコルが誤って解釈されたり，形式的検証の妨げとなったりするおそれがある．我々はこの問題に対処するべく，略式記法の構文を形式化し，Abadi とGordon のspi 計算への半自動的な変換を定義する．spi 計算は，暗号プロトコルの形式的記述・検証において最も成功している枠組みの1 つである．変換の基本方針は，プロトコルの各時点における各参加者の知識（どのような鍵，ノンス，識別子を知っているか）に基づき，各参加者の動作を明確化することである．

Security protocols are often defined in informal notations which have no clear semantics and only describe the message sequence when the protocol is successfully completed. This can be a source of incorrect interpretations of protocols as well as an obstacle to their formal verification. To address this problem, we formalize the syntax of the informal notations and present their semi-automatic translation into Abadi and Gordon’s spi-calculus, one of the most successful frameworks for the formal specification and verification of cryptographic protocols. Our main idea is to make the actions of each principal explicit on the basis of its knowledge, i.e., what keys, nonces and names it knows at each point in a protocol.

収録刊行物

• 情報処理学会論文誌プログラミング（PRO）

  情報処理学会論文誌プログラミング（PRO） 45 (SIG12(PRO23)), 1-10, 2004-11-15

  東京 : 情報処理学会

キーワード

• 通常論文

詳細情報

• CRID: 1050282812867257600
• NII論文ID: 110002768476
• NII書誌ID: AA11464814
• ISSN: 18827802
• ISSN: 03875806
• NDL書誌ID: 7158012
• Web Site: http://id.nii.ac.jp/1001/00016656/
• Web Site: https://ndlsearch.ndl.go.jp/books/R000000004-I7158012
• 本文言語コード: ja
• 資料種別: article
• データソース種別:
  • IRDB
  • NDL
  • CiNii Articles