WEKO3
アイテム
暗号プロトコルの形式記述に向けたLLMチャットボットの活用
https://ipsj.ixsq.nii.ac.jp/records/240779
https://ipsj.ixsq.nii.ac.jp/records/240779682908b2-1105-49ae-bbe4-12f79623b8b5
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-CSS2024033.pdf (322.4 kB)
2026年10月15日からダウンロード可能です。
|
Copyright (c) 2024 by the Information Processing Society of Japan
|
|
| 非会員：¥660, IPSJ:学会員：¥330, CSEC:会員：¥0, SPT:会員：¥0, DLIB:会員：¥0 | ||
| Item type | Symposium(1) | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2024-10-15 | |||||||||
| タイトル | ||||||||||
| 言語 | ja | |||||||||
| タイトル | 暗号プロトコルの形式記述に向けたLLMチャットボットの活用 | |||||||||
| タイトル | ||||||||||
| 言語 | en | |||||||||
| タイトル | Utilizing LLM Chatbots for Formal Descriptions of Cryptographic Protocols | |||||||||
| 言語 | ||||||||||
| 言語 | jpn | |||||||||
| キーワード | ||||||||||
| 主題Scheme | Other | |||||||||
| 主題 | 形式検証，暗号プロトコル，大規模言語モデル | |||||||||
| 資源タイプ | ||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_5794 | |||||||||
| 資源タイプ | conference paper | |||||||||
| 著者所属 | ||||||||||
| 日本電信電話株式会社NTTコミュニケーション科学基礎研究所 | ||||||||||
| 著者所属 | ||||||||||
| 九州大学大学院システム情報科学府 | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| NTT Communication Science Laboratories | ||||||||||
| 著者所属(英) | ||||||||||
| en | ||||||||||
| Kyushu University | ||||||||||
| 著者名 |
櫻田, 英樹
× 櫻田, 英樹
× 櫻井, 幸一
|
|||||||||
| 著者名(英) |
Hideki, Sakurada
× Hideki, Sakurada
× Kouichi, Sakurai
|
|||||||||
| 論文抄録 | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | 暗号プロトコルの安全性を検証する方法として形式検証がある．形式検証ではプロトコルの仕様と安全性を検証ツールと呼ばれるソフトウェアの入力言語によって記述することで自動的な検証が可能である．しかし一般にプロトコルの仕様と安全性は自然言語で記述・説明されており，ツールの言語で記述し直すことは専門的な知識と時間を要する．本研究ではLLMチャットボットを活用して暗号プロトコルの形式記述を効率的に作成することを試みた．具体的にはLLMチャットボットが自然言語で記述されたプロトコル仕様を理解し，これを形式的な記述に変換する過程を説明する．この手法を用いることで，形式検証ツールへの入力作成の最初のステップを支援し，形式検証ツールを使い始める際の労力を削減することを目指す． | |||||||||
| 論文抄録(英) | ||||||||||
| 内容記述タイプ | Other | |||||||||
| 内容記述 | Formal verification is a method used to verify the security of cryptographic protocols. In formal verification, the specifications of a protocol and its security properties are described using the input language of a software tool called a verification tool, enabling automated verification. However, protocol specifications and security properties are Formal verification is a method used to verify the security of cryptographic protocols. In formal verification, the specifications of a protocol and its security properties are described using the input language of a software tool called a verification tool, enabling automated verification. However, protocol specifications and security properties are generally described and explained in natural language, and rewriting them in the tool’s language requires specialized knowledge and time. This study attempts to efficiently create formal descriptions of cryptographic protocols by utilizing an LLM chatbot. Specifically, it explains the process by which the LLM chatbot understands protocol specifications described in natural language and converts them into formal descriptions. By using this approach, we aim to support the initial step of creating inputs for formal verification tools and reduce the effort required when starting to use such tools. |
|||||||||
| 書誌情報 |
コンピュータセキュリティシンポジウム2024論文集 p. 242-247, 発行日 2024-10-15 |
|||||||||
| 出版者 | ||||||||||
| 言語 | ja | |||||||||
| 出版者 | 情報処理学会 | |||||||||
