유ㆍ무선 네트워크의 활성화와 더불어 중요 자원 혹은 사용자 정보 보호를 위해 다양한 보안프로토콜들이 개발되고 있다. 하지만, 대부분의 많은 보안 프로토콜들은 개발된 후, 시간이 지남에 따라 점차 보안 취약점들이 하나둘 발견되고 있다. 본 논문에서는 안전한 보안프로토콜을 개발하기 위해, EKE 프로토콜 분석 예제를 통해, 설계단계에서 보안 프로토콜의 안전성을 검증하는 정형적 방법론에 대해 소개하고, 정형적 검증 방법론의 실효성을 보이기 위해, Casper 및 FDR 도구론 이용하여 BCY 프로토콜의 안전성을 분석한 후, 보안성을 향상시킨 새로운 BCY 프로토콜을 제안한다.
유ㆍ무선 네트워크의 활성화와 더불어 중요 자원 혹은 사용자 정보 보호를 위해 다양한 보안프로토콜들이 개발되고 있다. 하지만, 대부분의 많은 보안 프로토콜들은 개발된 후, 시간이 지남에 따라 점차 보안 취약점들이 하나둘 발견되고 있다. 본 논문에서는 안전한 보안프로토콜을 개발하기 위해, EKE 프로토콜 분석 예제를 통해, 설계단계에서 보안 프로토콜의 안전성을 검증하는 정형적 방법론에 대해 소개하고, 정형적 검증 방법론의 실효성을 보이기 위해, Casper 및 FDR 도구론 이용하여 BCY 프로토콜의 안전성을 분석한 후, 보안성을 향상시킨 새로운 BCY 프로토콜을 제안한다.
With the development of wire and wireless based networks, a various security protocols have been proposed to protect important resources and user information against attackers. However, many security protocols have found oかy to be later vulnerable to attacks. In this Paper, we introduce the formal m...
With the development of wire and wireless based networks, a various security protocols have been proposed to protect important resources and user information against attackers. However, many security protocols have found oかy to be later vulnerable to attacks. In this Paper, we introduce the formal methodology to verify the safety of security protocols in the design phase, and we take advantage of the formal methodology which uses Casper/CSP and FDR tools by introducing the verification example of EKE protocol and BCY protocol. Lastly, we propose a new BCY protocol after verifying it's safety.
With the development of wire and wireless based networks, a various security protocols have been proposed to protect important resources and user information against attackers. However, many security protocols have found oかy to be later vulnerable to attacks. In this Paper, we introduce the formal methodology to verify the safety of security protocols in the design phase, and we take advantage of the formal methodology which uses Casper/CSP and FDR tools by introducing the verification example of EKE protocol and BCY protocol. Lastly, we propose a new BCY protocol after verifying it's safety.
* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.
문제 정의
하지만, 이 논문에서는 서비 스 제공자와 사용자에게 공개키를 분배하는 제 3의 인증기관 S를 명세하지 않고, BCY 프로토콜의 안 전성을 검증하였다. Belief Logic을 기반으로한 GNY는 보안 프로토콜의 비밀성이나 인증속성을 증 명하기 보다는 상호 호스트의 믿음관계의 신뢰성을 증명하든데 그 목적이 있다. 따라서, Tom Coffey 의 논문은 BCY 프로토콜에서 V와 U 호스트가 세 션키 정보 SK1 과 SK2를 서로 신뢰하지 못한다는 사실을 증명하였다.
본 장에서는 간단한 EKE 프로토콜⑼ 명세 및 분 석 고]정을 통해, 모델체킹 방법 중에서도. Casper/ CSP 및 FDR을 이용한 보안 프로토콜 명세 및 검 증방법의 이해를 돕고자 한다.
FDR 모델체커 도구를 이용해서 BCY 프로토콜 이 위에서 언급한 비밀성 및 인증 속성을 만족하고 있는지 확인해 보았다. 그 결과 비밀성 (Secret(v, ru, [u]), Secret(u, ru, 〔v〕)) 및 인증 속성(Agr- eement(u, v, [ru, pkvd, sku〕))을 위반하는 보 안 취약점을 발견 할 수 있었다.
본 논문에서는 설계단계에서 보안 프로토콜의 안 전성을 검증하는 방법 및 도구를 분류 하였다. 그리 고 모델체킹 방법 중 널리 사용되고 있는 Casper/ CSP 및 FDR 도구를 이용하여 EKE 프로토콜 예 제를 분석 하는 과정을 상세히 보여줌으로써, 보안 프로토콜 검증 및 안전한 보안 프로토콜 설계에 대한 이해를 높이고자 하였다. 마지막으로, 무선 네트워크 환경에서 사용되는 BCY 프로토콜의 안전성을 분석 하고, 보안 취약성을 수정한 새로운 BCY 프로토콜 을 제안하였다.
제 2 장에서는 보 안 프로토콜의 안전성을 검증하기 위한 정형적 방법 론에 대해 소개한다. 그리고 Casper/CSP 및 FDR 도구를 이용한 EKE 프로토콜 안전성 분석 예제를 통해, 정형적 설계 및 검증 방법론에 대한 이해를 높 이고자 한다. 또한 무선 이동 네트워크 환경에서 사 용되는 BCY 프로토콜을 명세하고 검증한 사항을 언 급한다.
아 래 부분에서는 모델체킹 및 정리증명 방법에 대한 장 . 단점과 더불어 , 대표적인 보안 프로토콜 검증도 구들을 소개하고자 한다.
본 논문에서는 안전한 보안프로토콜을 설계하기 위한 연구내용에 초점을 맞추어, 지금까지 진행되어 오고 있는 보안 프로토콜 정형적 설계 및 검증 방 법론에 대해 소개하도록 하겠다. 특히, 그중에서도 Casper/CSP 및 FDR 도구를 이용한 검증 방법론 에 대해 상세히 언급하고자 한다
본 논문에서는 안전한 보안프로토콜을 설계하기 위한 연구내용에 초점을 맞추어, 지금까지 진행되어 오고 있는 보안 프로토콜 정형적 설계 및 검증 방 법론에 대해 소개하도록 하겠다. 특히, 그중에서도 Casper/CSP 및 FDR 도구를 이용한 검증 방법론 에 대해 상세히 언급하고자 한다
가설 설정
이와 마찬가지로 b는 메시지 를 수신하는 수신자 역할을 담당하며. b와 nb, passwd, kab 매개변수를 갖고 있으며, 다른 로스 트들의 공개키들과 자신만의 개인키를 알고 있다고 가정하고 있다.
그림 1은 BCY 프로토콜에 대한 Casper 명세 를 보여주고 있다. 그리고 본 논문에서는 암호 알고 리즘은 안전하기 때문에 공격자가 암호키를 알지 못 한 상태에서 암호문을 통해 암호키와 평문을 알아내 는 것은 불가능하다고 가정하고 있다.
보안 프로토콜의 메시지를 정형화 한다. 둘째, 최초의 가정을 명세한다.
공격자의 사전지식을 어떻게 구성하느냐에 따라, 보안 취약점 탐지 유무가 결정된다. 본 논문에서 BCY 프로토콜에대한 공격자 호스트의 이름은 Mallory 이며, 그는 모든 호스트 의 공개키, 자신의 개인키 그리고 Ru와 동일한 기능 을 하는 자신의 임의난수 세션키 Rm을 알고 있다고 가정하고 있다.
앞의 EKE 프로토콜 예제에서, 공격자의 이름은 Mallory 이며, 공격자는 각 호스트들의 이름인 Anne, Bob, Mallory, 자신이 생성하는 임의 난수 Nm, 모든 호스트들의 공개키 PK와 자신만의 개인키 SK(Mallory)를 알고 있다고 가정하고 있다.
제안 방법
- 본 장에서는 아래에 명세된 EKE 프로토콜 예제 를 통해, Caspei를 통해 명세된 각 섹션 헤더의 사 용법 및 의미 설명을 통해, 보안 프로토콜 표현 방법 을 구체적으로 보여주고자 한다.
첫째, 인증서버 S가 V와 U 에게 분배하는 인증서의 신뢰성을 높여, 재사용 공 격을 막도록 타임 스탬프를 추가하였다. 둘째, V와 U가 각각 Ru와 Rv 정보를 이용하여 세션키(SK) 를 생성하도록 수정하였다. 4번 메시어]서, ( + )는 XOR 연산을 이용한 Vernam 암호화 알고리즘을 나타내고 있다.
그리고 Casper/CSP 및 FDR 도구를 이용한 EKE 프로토콜 안전성 분석 예제를 통해, 정형적 설계 및 검증 방법론에 대한 이해를 높 이고자 한다. 또한 무선 이동 네트워크 환경에서 사 용되는 BCY 프로토콜을 명세하고 검증한 사항을 언 급한다. 마지막으로 결론을 맺고자 한다.
그리 고 모델체킹 방법 중 널리 사용되고 있는 Casper/ CSP 및 FDR 도구를 이용하여 EKE 프로토콜 예 제를 분석 하는 과정을 상세히 보여줌으로써, 보안 프로토콜 검증 및 안전한 보안 프로토콜 설계에 대한 이해를 높이고자 하였다. 마지막으로, 무선 네트워크 환경에서 사용되는 BCY 프로토콜의 안전성을 분석 하고, 보안 취약성을 수정한 새로운 BCY 프로토콜 을 제안하였다.
본 논문에서는 설계단계에서 보안 프로토콜의 안 전성을 검증하는 방법 및 도구를 분류 하였다. 그리 고 모델체킹 방법 중 널리 사용되고 있는 Casper/ CSP 및 FDR 도구를 이용하여 EKE 프로토콜 예 제를 분석 하는 과정을 상세히 보여줌으로써, 보안 프로토콜 검증 및 안전한 보안 프로토콜 설계에 대한 이해를 높이고자 하였다.
이 장에서는 Casper를 이용한 보안 프로토콜 검 증 방법의 이해를 돕기 위해, Casper 사용 매뉴얼 '⑷에 소개된 내용을 바탕으로 EKE 프로토콜의 안 전성 분석 예제를 소개하도록 하겠다.
BCY 프로토콜의 취약점을 개선하기 위해, 두 가 지사항을 고려하였다. 첫째, 인증서버 S가 V와 U 에게 분배하는 인증서의 신뢰성을 높여, 재사용 공 격을 막도록 타임 스탬프를 추가하였다. 둘째, V와 U가 각각 Ru와 Rv 정보를 이용하여 세션키(SK) 를 생성하도록 수정하였다.
이론/모형
FDR은 모델체 킹 도구로서, 대략 1"만큼의 상태 전이를 관찰할 수 있다. FDR 도구를 이용해서. CSP 언어로 구현
1 장에 기술한 BCY 프로토콜을 토대로, Casper■를 이용하여 BCY 프로토콜의 행위 및 보안 요구사항을 명세하였다. 본 논문에서는 추가적으로 인증기관 S의 행위도 Casper 모델에 추가하였다. Casper 모델은 기본적으로 8개의 헤더로 나누어지 지만, 중요한 #Protocol description, #Specifi- cation, #Intruder Knowledge 및 #Equival- ences 섹션 명세 부분에 대해서만 기술하도록 하겠 다.
성능/효과
V -> KU) : {{{NvHRm}}{PKm}}{SKui 위의 보안 취약점에서 I(V) 기호는Vendor로 위 장하거나 Vendor가 수신하는 메시지를 가로채는 공격자를 의미하게 된다. 결국, BCY 프로토콜의 보 안 취약점은 공격자가 V의 공개키 PKvd를 가로채 서 다시 이용하는 재사용 공격 (replay attack)이 가능하다는 것을 확인할 수 있었다. 이 공격을 방어 하기 위해서는 메시지에 타임 스탬프(timestamp) 를 표기하거나 혹은 인증서버에서 인증서 만료일을 알려주는 메시지를 보내주어 특정 시간이 지난 후 어】, V의 공개키를 재사용하는 취약점을 막아주어야 만 한다.
위의 강격시나리오를 통해, 중요 정보 (Nb)Kab가 공격자 Mallory에게 노출되는 것을 알 수 있고. 그 결과 EKE 프로토콜에서는 인증 속성을 만족하지 않는다 는 사실을 확인할 수 있다.
FDR 모델체커 도구를 이용해서 BCY 프로토콜 이 위에서 언급한 비밀성 및 인증 속성을 만족하고 있는지 확인해 보았다. 그 결과 비밀성 (Secret(v, ru, [u]), Secret(u, ru, 〔v〕)) 및 인증 속성(Agr- eement(u, v, [ru, pkvd, sku〕))을 위반하는 보 안 취약점을 발견 할 수 있었다.
셋째, 보안프로토콜의 목적 (goal)을 명세한다. 넷째, 논리 규칙을 적용한다.
수정된 BCY 프로토콜을 Casper/FDR 도구를 이용하여 검증한 결과 세션키 SK={Ru ( + ) Rv) 정보를 공격자가 가로챌 수 없고, V와 U는 세션키 를 이용하여 상호 호스트를 신뢰하고 인증할 수 있다 는 사실을 검증할 수 있었다.
Tom Coffey는 GNY를 이용하여 BCY 프로토콜의 안전성 검증하였다'⑹. 하지만, 이 논문에서는 서비 스 제공자와 사용자에게 공개키를 분배하는 제 3의 인증기관 S를 명세하지 않고, BCY 프로토콜의 안 전성을 검증하였다. Belief Logic을 기반으로한 GNY는 보안 프로토콜의 비밀성이나 인증속성을 증 명하기 보다는 상호 호스트의 믿음관계의 신뢰성을 증명하든데 그 목적이 있다.
참고문헌 (16)
박영희, 정병천, 이윤호, 김희열, 이재원, 윤현수, 'Diffie-Hellman 키 교환을 이용한 확장성을 가진 계층적 그룹키 설정 프로토콜,' 정보보호학회논문지, 13(5), pp. 3-15, 2003
권정옥, 황정연, 김현정, 이동훈, 임종인, '일방향 함수와 XOR을 이용한 효율적인 그룹키 관리 프로토콜 : ELKH,' 정보보호학회논문지, 12(6), pp. 93-112, 2002
G. Lowe, 'Breaking and Fixing the Needham-Schroeder Public-Key Protocol,' TACAS 96, pp. 147-166, 1996
P. E. Varner, 'Formal Methods as an Environmental Catalyst for Emergent Security in System Design and Construction,' December 12, 2002
M. Zalewski, 'Remote vulnerability in SSH daemon crc32 compensation attack detector,' Available from : http://razor.bindview.com/publish/advisories/adv_ssh1crc.html, February 2001
Formal Systems(Europe) Ltd. Failure Divergence Refinement-FDR2 User Manual, Aug. 1999
K. L. McMillian, 'Symbolic Model Checking,' PhD thesis, Carneigie Mellon University, May 1992
G. J. Holzman, 'The Model Checker SPIN,' IEEE Trans. on Software Engineering, vol. 23, Issue 5, pp. 279-295, May 1997
M. Burrows, M. Abadi and R. Needham. 'A Logic of Authentication,' In Proceeding of the Royal Society, Series A, 426, 1871, pp. 233-271, December 1989
L. Gong, R. Needham and R. Yahalom, 'Reasoning about Belief in Cryptographic Protocols,' Proceedings 1990, IEEE Symposium on Research in Security and Privacy, pp. 234-248, 1990
M. Bellovin and M. Merritt, 'Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks,' AT&T Bell Laboratories, Proceedings of the IEEE Computer Society Conference on Research in Security and Privacy, pp. 72-84, Oakland, 1992
G. Lowe, 'Casper: 'A compiler for the analysis of security protocols,' 10th IEEE Computer Security Foundations Workshop, 1997
Gavin Lowe, 'Casper : A Compiler for the Anaysis of Security Protocols,' User Manual and Tutorial, Version 1.3, 1999
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
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
※ AI-Helper는 부적절한 답변을 할 수 있습니다.