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

• Item type: Trans(1)
• 公開日: 2004-11-15
• タイトル: セキュリティプロトコルの略式記法からspi 計算への変換
• タイトル / 言語: en
• タイトル: Translating Security Protocols from Informal Notation into Spi Calculus
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 通常論文
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: ペンシルバニア大学コンピュータ情報科学科
• 著者所属: 東京大学情報理工学系研究科コンピュータ科学専攻
• 著者所属: 東京大学情報理工学系研究科コンピュータ科学専攻
• 著者所属(英): en
• 著者所属(英): Department of Computer and Information Science, University of Pennsylvania
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo
• 著者所属(英): en
• 著者所属(英): Department of Computer Science, Graduate School of Information Science and Technology, The University of Tokyo
• 著者名: 住井英二郎; 立沢, 秀晃; 米澤, 明憲
• 著者名(英): Eijiro, Sumii; Hideaki, Tatsuzawa; Akinori, Yonezawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: セキュリティプロトコルは往々にして非形式的な略式記法で定義されるが，この記法は明確な意味論がなく，プロトコルが正常に完了する場合のメッセージ列しか記述していない．そのためにプロトコルが誤って解釈されたり，形式的検証の妨げとなったりするおそれがある．我々はこの問題に対処するべく，略式記法の構文を形式化し，Abadi とGordon のspi 計算への半自動的な変換を定義する．spi 計算は，暗号プロトコルの形式的記述・検証において最も成功している枠組みの1 つである．変換の基本方針は，プロトコルの各時点における各参加者の知識（どのような鍵，ノンス，識別子を知っているか）に基づき，各参加者の動作を明確化することである．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: 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.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 45, 号 SIG12(PRO23), p. 1-10, 発行日 2004-11-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会