http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
전철욱(Chul-Wuk Jeon),김일곤(Il-Gon Kim),안영아(Young-a Ahn),김태규(Tae Kyu Kim),최진영(Jin-Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.1A
시스템이 대형화가 되어가고 네트워크 환경이 발전함에 따라 분산 환경이 점점 더 증대되어 가고 있다. 이러한 분산 환경에서 사용되는 리더 선출 알고리즘(Leader Election Algorithm)은 다양하게 제시 되었고 본 논문에서는 Garcia-Molina가 제시한 Bully 알고리즘을 프로세스 알제브라 언어인 CSP로 명세하고 FDR 모델체킹 도구를 이용해 해당 요구사항을 만족하는지 검증하였다.
전철욱(Chul-wuk Jeon),김일곤(Il-gon Kim),최진영(Jin-Young Choi),김상호(Sang-Ho Kim),노병규(Byung-Gyu Nho) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅰ
컴퓨터 통신이 확대되면서 심각하게 대두된 문제 중 하나는 보안 프로토콜의 설계와 구현이라 할 수 있다. 현재 안전한 보안 프로토콜을 설계하기 위해 정형 기법을 적용하여 검증하는 연구가 많이 진행되고 있다. 하지만 프로토콜을 설계 할 때 나타날 수 있는 보안적 취약 사항들을 정형 기법을 이용하여 제거한다 하더라도 구현된 프로토콜상에서 프로그래머의 코딩 실수나 프로그램 언어의 특성상 보안 취약점이 존재할 수 있다. 따라서 보안 프로토콜 구현시 나타날 수 있는 문제를 해결하기 위해 정형 검증된 프로토콜을 실제 구현 코드를 생성할 수 있는 도구의 필요성이 높아지고 있다. 본 논문에서는 Casper에서 보안 프로토콜을 검증한 후 검증된 프로토콜을 AISP-C2에 입력하여 C#으로 구현 코드를 자동 생성하도록 하고 정형 검증에서 검증할 수 없는 실제 컴퓨팅 환경에서 발생할 수 있는 보안성 취약점을 제거하기 위한 기능을 추가하였다.
전철욱(Chul-wuk Jeon),김일곤(Il-gon Kim),최진영(Jin-Young Choi),강인혜(In-Hye Kang),강필용(Pil-Yong Kang),이완석(Wan S. Lee) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ
최근 보안성의 취약점을 이용한 보안 사고들이 증가하고 있다. 이러한 보안적 취약점을 극복할 수 있는 방법으로 정형적 설계 및 검증이 있으며 그 필요성은 국외뿐만 아니라 국내에서도 점차적으로 늘어 나고 있다. 고등급의 보안 시스템을 개발하기 위해서는 정형화된 설계 및 검증 방법론을 사용해야 하지만 국내에서는 아직 정형적 설계 및 검증 방법에 대한 이해가 부족할 뿐만 아니라 개발 수준에서 보안성을 보다 쉽게 설계하고 안전성을 검증, 평가 할 수 있는 자동화 도구도 갖추어지지 않은 실정이다. 본 논문에서는 기존의 보안성을 정형적으로 설계하고 검증한 사례를 조사, 분류하여 국내 보안 시스템 개발자들이 활용할 수 있는 가이드를 만드는데 근간을 두고자 한다.
김일곤(Il-Gon Kim),전철욱(Chul-Wuk Jeon),김현석(Hyun-Seok Kim),최진영(Jin-Young Choi),강인혜(In-Hye Kang) 한국정보보호학회 2005 정보보호학회논문지 Vol.14 No.1
유ㆍ무선 네트워크의 활성화와 더불어 중요 자원 혹은 사용자 정보 보호를 위해 다양한 보안프로토콜들이 개발되고 있다. 하지만, 대부분의 많은 보안 프로토콜들은 개발된 후, 시간이 지남에 따라 점차 보안 취약점들이 하나둘 발견되고 있다. 본 논문에서는 안전한 보안프로토콜을 개발하기 위해, 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 only 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.
김일곤(Il-Gon Kim),김현석(Hyun-Suk Kim),전철욱(Chul-Wuk Jeon),이지연(Ji-Yeon Lee),최진영(Jin-Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅲ
무선 이동 시스템을 기반으로 안전한 키 교환 및 사용자 인증을 위한 다양한 보안 프로토콜이 제시되고 있다. 무선 이동 시스템 기반 보안프로토콜은 유선기반 보안프로토콜과 다르게 공개키와 대칭키가 혼합된 암호화 방식을 사용하고 있다. 본 논문에서는 이동 시스템 환경에서 동작하는 BCY 프로토콜의 안전성을 분석하기 위한 기술에 대해 언급하고, Casper/CSP 언어 및 FDR 도구를 이용하여 보안 취약성을 분석하고자 하였다.