@inproceedings{oai:ipsj.ixsq.nii.ac.jp:00240779,
 author = {櫻田, 英樹 and 櫻井, 幸一 and Hideki, Sakurada and Kouichi, Sakurai},
 book = {コンピュータセキュリティシンポジウム2024論文集},
 month = {Oct},
 note = {暗号プロトコルの安全性を検証する方法として形式検証がある．形式検証ではプロトコルの仕様と安全性を検証ツールと呼ばれるソフトウェアの入力言語によって記述することで自動的な検証が可能である．しかし一般にプロトコルの仕様と安全性は自然言語で記述・説明されており，ツールの言語で記述し直すことは専門的な知識と時間を要する．本研究ではLLMチャットボットを活用して暗号プロトコルの形式記述を効率的に作成することを試みた．具体的にはLLMチャットボットが自然言語で記述されたプロトコル仕様を理解し，これを形式的な記述に変換する過程を説明する．この手法を用いることで，形式検証ツールへの入力作成の最初のステップを支援し，形式検証ツールを使い始める際の労力を削減することを目指す．, 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.},
 pages = {242--247},
 publisher = {情報処理学会},
 title = {暗号プロトコルの形式記述に向けたLLMチャットボットの活用},
 year = {2024}
}