[논문]UPPAAL을 이용한 전자지불 프로토콜 분석

문영주; 방기석; 김일곤; 강인혜; 최진영

UPPAAL을 이용한 전자지불 프로토콜 분석
Analysis of E-Commerce Protocols Using UPPAAL 원문보기

문영주 (고려대학교 컴퓨터학과) , 방기석 (한림대학교 정보통신공학부) , 김일곤 (고려대학교 컴퓨터학과) , 강인혜 (서울시립대학교 기계정보공학과) , 최진영 (고려대학교 컴퓨터학과)

전자지불 시스템의 활용성 중대와 더불어 상거래의 안전성을 보장하는 문제가 중요한 핵심 사항으로 간주되고 있다. 본 논문에서는 이러한 전자지불 시스템의 암호화 키는 안전하다는 가정 하에 전자지불 프로토콜을 통해 소비자와 상인, 은행간의 상거래의 정확성을 중점으로 NetBill 프로토콜을 명세, 검증했다. 프로토콜의 명세를 위해서는 실시간 개념이 포함되어 있는 UPPAAL을 사용했다.

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

문제 정의

본 논문에서는 이러한 전자지불 시스템의 프로토콜의 암호화 키는 안전하다는 가정하에 전자지불 프로토콜을 소비자와 거래 상인 간의 상거래 정확성을 중점으로 NetBill 프로토콜을 검증하고자 한다. 즉, 프로토콜 구성 모듈들이 안전한 통신을 통해 상거래의 기본 요구사항이 올바르게 보장되는지 검증하고자 한다.
본 논문에서는 이러한 전자지불 시스템의 프로토콜의 암호화 키는 안전하다는 가정하에 전자지불 프로토콜을 소비자와 거래 상인 간의 상거래 정확성을 중점으로 NetBill 프로토콜을 검증하고자 한다. 즉, 프로토콜 구성 모듈들이 안전한 통신을 통해 상거래의 기본 요구사항이 올바르게 보장되는지 검증하고자 한다. 프로토콜의 명세를 위해서 실시간 개념이 포함되어 있는 Timed automata[4] 기반의 모델 체커인 UPPAAL[5] 을 사용하였다.

가설 설정

본 논문에서는 전자상거래에서 사용하는 전자지불 프로토콜의 암호화 키가 안전하다는 가정하에 프로토 콜의 참여 모듈 간의 상거래 행위를 중점으로 NetBill 프로토콜을 명세하였다. 전자상거래의 실제 상황에서 일어날 수 있는 시간 만료에 의한 예외 상황을 표현하기 위해 전자지불 프로토콜의 명세는 시간제한 사 항을 표현할 수 있는 Timed automata를 기반으로 하고 있는 UPPAAL을 사용하였다.

제안 방법

UPPAALe 기술 언어, 시뮬레이터, 모델 체커로 구성되어 있으며, 이들은 각각 시스템 에디터, 시뮬레이터, 검증기능을 제공한다. 기술 언어는 각 프로세스를 Timed automata로 표현한 것으로, 시스템 편집기를 이용해서 도식적으로 시스템을 명세하고, 시뮬레이터는 기술 언어로 표현된 시스템의 동적인 실행을 시뮬레이션해 서 시스템의 동작을 확인할 수 있게 해 주며, 모델 체 커는 명세 된 시스템의 상태 공간을 탐색해서 시스템이 만족해야 할 속성을 만족하는지 검증한다.
그림 1의 메시지 순서도와 비교해서 보면, 소비자가 상인에게 보내는 상품 요청 메시지는 그림 2에서 송신 이벤트로, 상인이 소비자에게 보내는 암호화된 물품 메시지는 수신 이벤트로 표현했다. 또한 소비자 프로토콜의 시간 만료를 표현하기 위해 로컬 클럭을 정의해서 한 정자에서 사용하도록 했다.
노드의 전이는 동기화 이벤트 외에 한 정차 (guard)에 의해 영향을 받는다. 한정 자는 각 프로세쓰 의 시간 변수에 대해 지연이나 시간 만료와 같은 시찬' 제약 사항을 표현하는 것으로, 제안된 모델은 시간제 약 사항에 따른 모델 검증이 가능하다.

이론/모형

본 논문에서는 전자상거래에서 사용하는 전자지불 프로토콜의 암호화 키가 안전하다는 가정하에 프로토 콜의 참여 모듈 간의 상거래 행위를 중점으로 NetBill 프로토콜을 명세하였다. 전자상거래의 실제 상황에서 일어날 수 있는 시간 만료에 의한 예외 상황을 표현하기 위해 전자지불 프로토콜의 명세는 시간제한 사 항을 표현할 수 있는 Timed automata를 기반으로 하고 있는 UPPAAL을 사용하였다.
즉, 프로토콜 구성 모듈들이 안전한 통신을 통해 상거래의 기본 요구사항이 올바르게 보장되는지 검증하고자 한다. 프로토콜의 명세를 위해서 실시간 개념이 포함되어 있는 Timed automata[4] 기반의 모델 체커인 UPPAAL[5] 을 사용하였다.

성능/효과

전자지불 프로토콜의 암호화 알고리즘이 안전하다는 가정하에, 프로토콜이 정확하게 동작했다면 소비자는 지불한 가치에 해당하는 물품을, 상인은 판매한 물품에 해당하는 가치를 얻어야 한다. UPPAAL을 사용하여 검증한 결과, NetBill 프로토콜이 상거래의 기본 요구 사항을 만족시켜 준다는 사실을 확인하였다.

후속연구

향후에는 CEPS 전자지갑 표준을 기반으로 한 전자 상거래 시스템의 전자화폐 구입 및 충전 기능의 안전성을 검증할 예정이다.

원문 보기

ScienceON 원문보기

*원문 PDF 파일 및 링크정보가 존재하지 않을 경우 KISTI DDS 시스템에서 제공하는 원문복사서비스를 사용할 수 있습니다.

이 논문과 함께 이용한 콘텐츠

[논문] Dictionary Attack 방지를 위한 S/KEY 설계 및 구현

내보내기 메뉴

내보내기 구분

파일저장
인쇄
메일전송

구성항목

기본정보
상세정보

관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관

저장형식

Text(ASCII format)
Excel format
RefWorks Direct Export
RIS format (for Reference Manager, ProCite, EndNote), Scholar's Aids, Mendeley

메일정보

받는사람 (필수): @
보내는사람 (선택): @
제목
내용: KISTI 검색결과 이메일 서비스

안내

총 건의 자료가 검색되었습니다.

다운받으실 자료의 인덱스를 입력하세요. (1-10,000)

검색결과의 순서대로 최대 10,000건 까지 다운로드가 가능합니다.

데이타가 많을 경우 속도가 느려질 수 있습니다.(최대 2~3분 소요)

다운로드 파일은 UTF-8 형태로 저장됩니다.
파일의 내용이 제대로 보이지 않을실 때는 웹브라우저 상단의 보기 -> 인코딩 -> 자동선택 여부를 확인하십시오.

Text(ASCII format)
Excel format

표제어: PCR

동의어: Packet Collision Rate

용어 설명 출처 목록 (6)

용어 설명: PCR은 세균 특이성이 있는 primer를 이용하여 적은 수의 세균이 있을지라도 쉽게 검출할 수 있는 유용한 방법이며, 이를 이용하여 구강 내 치면세균막이나 타액에서 직접 세균을 검출할 수 있게 되었다[8].

AI-Helper ※ AI-Helper는 을 사용합니다.

AI-Helper

안녕하세요, AI-Helper입니다. 좌측 "선택된 텍스트"에서 텍스트를 선택하여 요약, 번역, 용어설명을 실행하세요.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.

연합인증

UPPAAL을 이용한 전자지불 프로토콜 분석
Analysis of E-Commerce Protocols Using UPPAAL 원문보기

초록
AI-Helper