Z를 이용한 보안기능의 설계 방법 연구 = Formal specification for secure functions using Z

국문 초록 (Abstract)

본 논문에서는 정형 명세 언어 Z를 이용한 보안 관련 MD4 Message Digest 알고리즘에 대한 정형 명세 방법론을 제시하였다. 현대 사회는 인터넷 기술의 발달로 인하여 통신상에서의 전자 상거래가 시작되었고, 그 이용도는 급속하게 늘어나고 있다. 전자 상거래 시스템이 운영되면서 가장 중요한 문제로 서비스를 이용하는 사용자들에 대한 사용자 정보 보안과 보안 시스템에 접근하는 사용자가 정상적인 사용자인지를 확인하기 위한 사용자 인증이 부상되고 있다 이 문제를 해결하기 위해서 보안에 관련된 많은 암호화 기법과 알고리즘이 개발되고 있고, 전세계적으로 이런 알고리즘으로 구현된 보안 상품의 등급을 나누고 있다. 그 예로 미국의 NIST(National Institute of Standards and Technology), 영국의 통신정보국(GCHQ)등과 같은 기관에서 시스템에 대한 등급을 판단하고, 우리나라에서도 정보보호센터에서 K1에서 K7까지의 등급을 주고 있다. 이런 보안 등급에서 일반적으로 정형기법을 사용하여 구현된 보안 상품이 최상의 평가를 받고 있다. 따라서, 전자 상거래 시스템을 구현하는 개발자 입장에서는 보안 시스템 구현에 정형기법을 이용하여 고품질의 상품을 만드는 것이 중요하다. 하지만, 국내에서는 이러한 분야에 대한 연구가 전무한 상태여서 어떠한 기준을 적용하는 것이 좋은 지를 판단하기가 매우 어려운 실정이다 따라서, 본 논문에서는 이러한 문제에 대한 연구로 정형 명세 언어를 이용해서 인증 알고리즘을 명세하는 방법론을 적용한 경험을 기술한다.

다국어 초록 (Multilingual Abstract)

In this paper, we describe a experience of applying formal specification methodology to MD(Message Digest) 4 algorithm, a part of secure algorithm, with formal specification language Z. Recently, Internet start the Electronic Commerce(EC) service and its utilization is increased very rapidly. The most important problem of Electronic Commerce System(ECS) are preservation of user's information and authentication of user To solve this problems, many cryptography methodologies and algorithms are developed. Many country grade developed secure system with such algorithm. for example, NIST of Unite State and GCHQ of British grade secure system. In our country, Korea Information Security Agency grade K1 to K7. In secure grade, Secure system using formal methods get more high grade than others. So, using formal methods is great issue for developer of ECS. But, our country doesn't have any experience of such area. So, this paper describe a experience of specification methodology for authentication algorithm with formal specification language

목차 (Table of Contents)

• 1. 서론
• 2. 정형기법(Formal Methods)
• 2.1 정형 명세(Formal Specification)
• 2.2 정형 검증(Formal Verification)
• 3. 정형 명세 언어 Z
• 3.1 Z의 기본적인 문법
• 3.2 Z를 이용한 명세 방법론
• 4. MD4 Message Digest 알고리즘
• 4.1 해시 함수(Hash function)
• 4.2 전자 서명
• 4.3 MD4 Message Digest 알고리즘
• 5. Z를 이용한 MD4 Message Digest Algorithm 명세
• 5.1 데이터 타입, 집합과 전역상수에 대한 명세
• 5.2 추상화 상태(Abstract state)에 대한 명세
• 5.3 동작(Operation)에 대한 명세
• 5.4 정형 명세 언어 Z로 명세한 경험
• 6. 결론