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 make 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.