2024-03-28T22:37:48Zhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_oaipmhoai:ipsj.ixsq.nii.ac.jp:001469252023-11-14T00:51:14Z06164:06165:06462:08443
ProVerifによるTLS1.3ハンドシェイクプロトコルの形式検証Formal Verification of TLS 1.3 Handshake Protocol Using ProVerifjpnCSS,TLS1.3,ハンドシェイクプロトコル,形式検証,ProVerifhttp://id.nii.ac.jp/1001/00146892/Conference Paperhttps://ipsj.ixsq.nii.ac.jp/ej/?action=repository_action_common_download&item_id=146925&item_no=1&attribute_id=1&file_no=1Copyright (c) 2015 by the Information Processing Society of Japan東京理科大学株式会社日立製作所研究開発グループ日本電信電話株式会社NTTコミュニケーション科学基礎研究所荒井, 研一渡辺, 大櫻田, 英樹ProVerif は Blanchet らが開発した形式モデルでの暗号プロトコルの自動検証ツールであり,暗号プロトコルで要求される秘匿や認証などの安全性を検証可能である.一方,TLS(Transport Layer Security) はインターネット上で安全な通信を提供する暗号プロトコルであり,ハンドシェイクプロトコルは相手認証及び安全な通信を確立するために必要なセキュリティパラメータのネゴシエーションを行うプロトコルである.本稿では,ProVerif を用いて TLS1.3(TLS protocol version 1.3) ハンドシェイクプロトコルを形式的に記述し,安全性検証を行う.ProVerif is an automatic cryptographic protocol verifier based on the formal model developed by Blanchet et al. This verifier can verify the properties of secrecy and authentication, etc. On the other hand, TLS (Transport Layer Security) is a cryptographic protocol that provides communications security over the Internet. The handshake protocol is a protocol that provides a means of authentication and the negotiation of security parameters in TLS. In this paper, we introduce our formalization of the TLS 1.3 (TLS protocol version 1.3) handshake protocol and verify its security using ProVerif.コンピュータセキュリティシンポジウム2015論文集20153100310102015-10-142015-12-18