SSLプロトコルの形式仕様記述と検証

IPSJ Web Site 12 References

Bibliographic Information

Other Title
  • SSL プロトコル ノ ケイシキ シヨウ キジュツ ト ケンショウ
  • Formal Specification and Verification of the SSL Protocol

Search this article

Description

通信の安全性が保証されていないインターネットのようなネットワーク上で 安全な通信を実現するために「セキュリティプロトコル」が利用されている.セキュリティプロトコルが安全な通信を実現していることを示すには プロトコルがどのような前提条件を想定していて 何を保証しているのかを明確にすることが重要である.本研究の目的は 形式手法によるセキュリティプロトコルの仕様記述法および検証法を提示することにより セキュリティプロトコルの安全性を明確にすることである.本研究では 形式手法RAISEを用いてセキュリティプロトコルの記述を行い プロトコルが保証している安全性を明確にし 安全性に対する形式的な証明を与えることで安全性の保証を図る.本論文では SSLプロトコルを対象として RSLによるプロトコルの仕様記述 およびSSLプロトコルが想定しているサーバへのなりすまし攻撃に対する安全性の検証法を示す.セキュリティプロトコルの仕様を形式的に厳密に定義することにより プロトコルが想定している前提条件が明示的に記述され プロトコルが保証している安全性が明確になる.

Security protocols are used to establish secure connections between computers over an insecure network such as the Internet. One of the most important issues is to make clear what kind of precondition a security protocol assumes and what kind of property is guaranteed by the protocol. Our goal is to make security properties clear by presenting formal methods for specification and verification of security protocols. We intend to describe formal specification of a security protocol using the RAISE method, and to make security properties clear which the protocol intends to guarantee. We also to give formal proof of the properties and guarantee that the protocol has them. In this paper, we specify the SSL Protocol using RSL and verify its security against the man-in-the-middle attack which is supposed to be done against the protocol. As we describe formal and rigorous specification of the protocol. We can obtain clear preconditions which the protocol assumes, and make clear what kind of property the protocol guarantees.

Journal

References(12)*help

See more

Keywords

Details 詳細情報について

Report a problem

Back to top