지금까지의 많은 보안프로토콜들은 비정형화된 설계 및 검증 방법을 통해 개발되었다. 그 결과 유.무선 네트워크 분야에서 보안상 안전하다고 여겨왔던 많은 보안 프로토콜들의 보안 취약점들이 하나둘씩 발견되어오고 있다. 이에 따라, 통신 프로토콜을 개발하기 이전에 설계단계에서부터, 수학적인 기호 및 의미에 바탕을 둔 설계 언어로, 프로토콜의 안전성을 분석하기 위한 정형적 설계 및 검증 방법의 중요성이 점차 증대되고 있다. 현재, 모바일 통신 네트워크의 확산과 더불어 다양한 모바일 프로토콜들이 제안되고 있다. 본 논문에서는 정형적 검증 방법을 이용해서 ASK 모바일 프로토콜의 보안 취약점을 지적한다. 또한, 보안 취약점을 개선한 새로운 ASK 모바일 프로토콜을 제안하고 검증하였다.
지금까지의 많은 보안프로토콜들은 비정형화된 설계 및 검증 방법을 통해 개발되었다. 그 결과 유.무선 네트워크 분야에서 보안상 안전하다고 여겨왔던 많은 보안 프로토콜들의 보안 취약점들이 하나둘씩 발견되어오고 있다. 이에 따라, 통신 프로토콜을 개발하기 이전에 설계단계에서부터, 수학적인 기호 및 의미에 바탕을 둔 설계 언어로, 프로토콜의 안전성을 분석하기 위한 정형적 설계 및 검증 방법의 중요성이 점차 증대되고 있다. 현재, 모바일 통신 네트워크의 확산과 더불어 다양한 모바일 프로토콜들이 제안되고 있다. 본 논문에서는 정형적 검증 방법을 이용해서 ASK 모바일 프로토콜의 보안 취약점을 지적한다. 또한, 보안 취약점을 개선한 새로운 ASK 모바일 프로토콜을 제안하고 검증하였다.
Security protocols have usually been developed using informal design and verification techniques. However, many security protocols thought to be secure was found to be vulnerable later. Thus, the importance of formal specification and verification for analyzing the safely of protocols is increasing....
Security protocols have usually been developed using informal design and verification techniques. However, many security protocols thought to be secure was found to be vulnerable later. Thus, the importance of formal specification and verification for analyzing the safely of protocols is increasing. With the rise of mobile communication networks, various mobile security protocols have been proposed. In this paper, we identify the security weakness of the ASK mobile Protocol using formal verification technique. In addition, we propose a new ASK protocol modifying its vulnerability and verify its robustness.
Security protocols have usually been developed using informal design and verification techniques. However, many security protocols thought to be secure was found to be vulnerable later. Thus, the importance of formal specification and verification for analyzing the safely of protocols is increasing. With the rise of mobile communication networks, various mobile security protocols have been proposed. In this paper, we identify the security weakness of the ASK mobile Protocol using formal verification technique. In addition, we propose a new ASK protocol modifying its vulnerability and verify its robustness.
* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.
문제 정의
본 논문에서는 Casper/FDR 도구를 이용한 정형적 설계 및 검증방법을 사용하여, ASK 모바일 보안 프로토콜의 보안 취약점을 지적한다. 그리고 안전한 상호 키 교환 및 사용자 인증을 제공하는 새로운 ASK 모바일 프로토콜을 검증하고 제안하고자 한다.
본 논문에서는 Casper/FDR 도구를 이용한 정형적 설계 및 검증방법을 사용하여, ASK 모바일 보안 프로토콜의 보안 취약점을 지적한다. 그리고 안전한 상호 키 교환 및 사용자 인증을 제공하는 새로운 ASK 모바일 프로토콜을 검증하고 제안하고자 한다.
하지만, 대부분의 경우 비정형화된 설계 및 검증방법을 통해 개발되기 때문에 나중에 보안상 취약점이 발견되고 있다. 본 논문에서는 모델체킹 기법을 이용하여 ASK 모바일 프로토콜의 보안 취약점을 지적하였다. 뿐만 아니라, 보안 취약점을 개선한 새로운 ASK 프로토콜을 제안하고 검증하였다.
본 논문에서는 모델체킹 방법을 이용하여 ASK 모바일 프로토콜의 취약점을 분석하고, 보안성이 강화된 새로운 프로토콜을 제안한다.
#Specification 섹션 헤더는 검증하고자 하는 보안 속성을 정의한다. 본 논문에서는 비밀성(confidentiality)과 인증(authentication), 두 가지의 보안 속성을 검증하였다. Casper에서 'Secret' 표현식은 비밀성 속성올 정의 하기 위해 사용된다.
가설 설정
예를 들어, 위의 명세 코드를 보면 공격자 호스트의 이름은 Mallory라고 설정하였으며, Vendor, User 그리고 Sam은 각각 V, U 그리고 S 호스트에 대한 도메인 이름을 나타내고 있다. 본 논문에서는 공격자는 모든 호스트의 식별자 및 공개키 정보를 알고 있고, 자신의 임의 난수 Rm과 자신의 개인키 키 SKm을 알고 있다고 가 정한다.
수정된 ASK 프로토콜을 이용하여, 앞의 5장에서 언급한 바와 같이, 사용자가 모바일 통신 디바이스를 이용하여 유료 컨텐츠를 다운로드 하는 경우를 가정해 보자. 1번과 2번 메시지를 이용하여 인증기관은 서비스 제공자와 사용자의 모바일 통신 디바이스에 각각 인증서를 분배하게 된다.
제안 방법
Casper와 FDR 도구를 이용하여, 수정된 ASK 프로토콜의 비밀성 및 인증 속성을 검증하였다. Casper에서 명시한 두 가지 보안 속성은 다음과 같다.
Ghezzi와 Kemmerer^ ASTRAL 모델체킹 도구를 이용하여 TMN 모바일 프로토콜의 취약점을 발견하였다[4]. Coffey와 Dojen은 정리증명 방법에 기반을 둔 GNY 로직을 이용하여, BCY 모바일 프로토콜의 보안 취약점을 지적하고 새로운 CDF-BCY 프로토콜을 제안 하였다[5].
넷째, FDR 도구의 검증결과를 분석한다.
둘째, 사용자와 서비스 제공자의 인증서, CertV와 CertU의 재사용 공격을 방지하기 위해서 인증서의 만기 시간을 나타내는 변수 TSv와 TSu를 각각 첨가하였다. 만일 공격자가 사용자 및 서비스 제공자 사이의 메시지를 가로채어 재사용 하게 되면, 인증서에 표기된 타임 스탬프를 통해 사용자와 서비스 제공자는 메시지의 재사용 여부를 확인할 수 있게 된다.
본 논문에서는 모델체킹 기법을 이용하여 ASK 모바일 프로토콜의 보안 취약점을 지적하였다. 뿐만 아니라, 보안 취약점을 개선한 새로운 ASK 프로토콜을 제안하고 검증하였다.
셋째, 세션키의 안전성을 강화하기 위해 사용자의 임의 난수 Ru를 첨가하였다. 수정된 ASK 프로토콜의 새로운 세션키는 h(ru, rv)가 된다.
이론/모형
인증 속성은 단방향 인증 및 양방향 언증 측면으로 나누어 검증할 수 있다. 본 논문에서는 사용자 U와 서비스 제공자 V간의 상호 인증관계를 검증하기 위해 lAgreement(v, u, [rvt pku, skv])'와 , Agreement(u, v, [rv, pkv, sku])' 표현식을 사용하였다.
성능/효과
FDR 도구를 통해 검증해 본 결과, 수정된 ASK 프로토콜은 위에서 정의한 보안 속성들을 모두 만족하고 있음을 확인할 수 있었다. 공격자는 사용자의 임의 난수 Ru 정보를 가로챌 수 없기 때문에, 결국 사용자와 서비스 제공자는 세션키와 Diffie-Hellman 키를 이용해서 상호 호스트를 인증하게 된다.
새롭게 제안된 ASK 프로토콜은 기존의 프로토콜에 비해 적은 메시지 교환 횟수를 갖기 때문에 낮은 연산 속도와 적은 양의 배터리를 사용하는 모바일 통신 환경에 적합한 것으로 사료된다. 또한 보안상 기존의 ASK 프로토콜에 비해 더 안전하다는 것을 검증하였다.
첫째, 검증하고자 하는 보안프로토콜을 Casper 도구로 명세한다.
후속연구
마지막으로 보안프로토콜의 취약점이 밝혀지면, 문제점을 수정하여 동일한 설계 및 검증절차를 반복 수행 한다.
향후 연구과제로는 본 논문에서 새롭게 제안하는 프로토콜과 기존의 ASK 프로토콜의 네트워크 속도에 따른 성능을 비교 및 분석 하고자 한다.
참고문헌 (13)
G. Lowe, 'Breaking and Fixing the Needham-Schroeder Public-Key Protocol,'TACAS 96, pp.147-166, 1996
I. G. Kim and J. Y. Choi, 'Formal verification of PAP and EAP- MD5 Protocols in wireless networks : FDR Model Checking,' 18th AINA, pp.264-269, 2004
A. Roscoe and M. Goldsmith, 'The Perfect Spy for Model-Checking Cryptoprotocols,' Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997
Z. Dang, 'Using the ASTRAL Model Checker for Cryptographic Protocol Analysis,' Proceedings of the 1997 DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997
T. Coffey and R. Dojen, 'Analysis of a mobile communication security protocol,' Proceeding of the 1st international symposium on Information and communication technologies, pp. 322-328, 2003
C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall, 1985
P. Y. A. Ryan and S. A. Schneider, modelling and analysis of security protocols: the CSP Approach, Addison-Wesley, 2001
G. Lowe, 'Casper: A Compiler for the Analysis of Security Protocols,' 10th IEEE Computer Security Foundations Workshop, 1997
Formal Systems (Europe) Ltd. Failure Divergence Refinement-FDR2 User Manual. 1999
M. Aydos, B. Sunar, and C. K. Koc, 'An elliptic curve cryptography based authentication and key agreement protocol for wireless communication,' presented at the 2nd Int. Workshop Discrete Algorithms and Methods for Mobility, Dallas, TX, Oct. 1998
M. J. Beller, L. -F. Chang and Y. Yacobi, 'Privacy and authentication on a portable communications system,' Proceedings of the International Computer Symposium, Vol.1, pp.821-829, 1994
A. Aziz and W. Diffie, 'Privacy and authentication for wireless local area networks,' IEEE Personal Commun., First Quarter 25 31, 1994
※ AI-Helper는 부적절한 답변을 할 수 있습니다.