암호프로토콜 논리성 자동 검증에 관한 연구

Vol. 13, No. 1, pp. 115-130, 2월. 2003
10.13089/JKIISC.2003.13.1.115, Full Text:
Keywords: 인증 프로토콜, 프로토콜 분석, 인증 로직
Abstract

본 논문에서는 암호프로토콜의 논리성 검증을 위한 방법 중 하나인 SVO 로직을 바탕으로 한 자동 검증 방법과 실험에 대해서 다룬다. 먼저 기존 SVO 로직 자동 검증의 문제점을 도출한 후 자동 검증을 고려한 ASVO 로직을 설계하고 검증하였으며, Isabelle/Isar 시스템을 이용하여 구현하였다 본 논문에서는 잘 알려진 NSSK 프로토콜 중심으로 추론 구성 사례를 소개하도록 한다. 결과적으로 이미 Denning-Sacco 공격에 취약한 것으로 알려진 NSSK 프로토콜의 문제점들을 ASVO 로직의 자동화 검증을 통해서 정확히 확인할 수 있었다. 그리고 최종적으로 ASVO 로직의 자동화 검증을 통해서 발견된 취약점들을 개선한 NSSK7 프로토콜을 설계하고 검증하였다.

Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from December 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
권태경, 양숙현, 김승주 and 임선간, "An Experimental Study on the Semi-Automated Formal Verification of Cryptographic Protocols," Journal of The Korea Institute of Information Security and Cryptology, vol. 13, no. 1, pp. 115-130, 2003. DOI: 10.13089/JKIISC.2003.13.1.115.

[ACM Style]
권태경, 양숙현, 김승주, and 임선간. 2003. An Experimental Study on the Semi-Automated Formal Verification of Cryptographic Protocols. Journal of The Korea Institute of Information Security and Cryptology, 13, 1, (2003), 115-130. DOI: 10.13089/JKIISC.2003.13.1.115.