[논문]자동차 보안시스템에서 장치간 상호인증 및 정형검증

이상준; 배우식

doi:10.14400/jdc.2015.13.4.205

초록
AI-Helper

자동차산업의 발전과 함께 M2M(Machine-to-Machine)통신이 자동차 산업분야에서 많은 관심이 되고 있다. M2M은 기상, 환경, 물류, 국방, 농.축산 등에서 사용하기 시작하여 장비들이 자동으로 상황에 맞추어 통신을 하고 상황에 맞는 동작을 함으로써 운영해가는 시스템이다. 자동차에서도 차량내부 장치 간, 차대 차, 차와 교통시설물, 차와 주변의 환경 등에 적용되고 있다. 그러나 통신시스템의 특성상 전송구간에서 공격자의 공격에 대한 문제가 있으며 자동차의 운행, 제어계통 및 엔진제어 등에 공격자의 공격이 진행되면 안전에 심각한 문제가 발생하게 된다. 따라서 디바이스 간 보안통신에 대한 연구가 활발히 진행되고 있다. 본 논문에서는 차량의 디바이스간 안전한 통신을 위해 해시함수 및 수학적 복잡한 공식을 이용하여 프로토콜을 설계하였으며 프로토콜 정형검증 도구인 Casper/FDR을 이용하여 실험하였으며 제안한 프로토콜이 각종 공격에 안전하게 동작되며 실제 적용할 때 효과적임을 확인하였다.

Abstract ▼ AI-Helper

The auto industry has significantly evolved to the extent that much attention is paid to M2M (Machine-to-Machine) communication. In M2M communication which was first used in meteorology, environment, logistics, national defense, agriculture and stockbreeding, devices automatically communicate and op...

The auto industry has significantly evolved to the extent that much attention is paid to M2M (Machine-to-Machine) communication. In M2M communication which was first used in meteorology, environment, logistics, national defense, agriculture and stockbreeding, devices automatically communicate and operate in accordance with varying situations. M2M system is applied to vehicles, specifically to device-to-device communication inside cars, vehicle-to-vehicle communication, communication between vehicles and traffic facilities and that between vehicles and surroundings. However, communication systems are characterized by potential intruders' attacks in transmission sections, which may cause serious safety problems if vehicles' operating system, control system and engine control parts are attacked. Thus, device-to-device secure communication has been actively researched. With a view to secure communication between vehicular devices, the present study drew on hash functions and complex mathematical formulae to design a protocol, which was then tested with Casper/FDR, a tool for formal verification of protocols. In brief, the proposed protocol proved to operate safely against a range of attacks and be effective in practical application.

주제어

AI 본문요약
AI-Helper

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

문제 정의

이는 자동차 분야에서는 생명과도 직결된 문제로 중요한 분야이다. 본 논문에서는 자동차 M2M 통신에서 보안 문제를 해결하기 위해 보안적으로 안전하고 효율적인 통신 프로토콜을 제안하였다. 해시 연산과, 공개키 및 비밀키를 사용하였으며 #연산을 기본으로 설계하여 상호 인증을 제공하고 있다.
본 논문에서는 최근 정형검증 분야에서 많이 사용하는 Casper/FDR[12,13] 도구를 사용하여 제안한 프로토콜을 검증실험 하였으며 M2M 시스템에서 안전한 통신 프로토콜임이 증명되었다. 본 논문의 구성은 다음과 같다.

제안 방법

프로토콜의 보안성 확인 부분으로 제안한 프로토콜이 공격자에게 안전함을 나타낸다. 검증한 Agent간 통신과 데이터값과 세션키의 보안성이 안전한지 확인하였다.
본 논문에서는 매 세션 바뀌는 난수와 변수 값을 이용하고 실시간 에이전트 값 및 해시함수를 기반으로 설계하였다. 기호의 정의는 [Table 1]과 같다.
본 논문에서는 연구용 FDR 2.91 버전의 모델검증 프로그램을 사용하여 설계한 자동차 보안 M2M 프로토콜의 안전성, 교착상태, 라이브락 등의 동작을 검증하였다. [Fig.
프로그램을 실행시키면 자동으로 CSP 문서로 변환시켜 준다. 이렇게 변환된 CSP 문서를 FDR(Failure Divergence Refinements) 프로그램을 이용하여 보안성과 인증속성과 같은 보안속성을 만족하는지 검증하며 FDR 에서는 safety 검증, deadlock 검증, livelock 검증을 확인하며 보안상 취약점이 발견되면 어떤 공격 시나리오가 가능한지 보여주어 취약점 분석이 쉽도록 되어있다. 아울러 FDR에서는 추적모델, 실패모델, 실패/분기모델을 지원한다[16].

성능/효과

1) 인증 및 데이터 무결성 : 차량 통신에서 개체가 자신이 정당한 소유자임이 확인되어야 하는데 이를 충족하기 위해 모든 개체는 유일한 ID를 가져야 한다.
3) 익명 및 프라이버시 : 차량 통신에서 익명성이 결여 되면 프라이버시 침해의 위험이 존재한다. 따라서 프라이버시 보호방안이 제공되지 않는다면, 공격자가 차량의 주행, 위치, 영상 등 정보를 확인하며 심각한 문제가 발생할 수 있다.
3), 4)는 k, x 의 Responder와 Initiator가 서로 정상적인 통신으로 상호 인증할 수 있는지 검증하는 부분으로 결과 값과 같이 에이전트 간 안전하게 상호 인증함을 확인하였다.
해시 연산과, 공개키 및 비밀키를 사용하였으며 #연산을 기본으로 설계하여 상호 인증을 제공하고 있다. Casper/FDR 정형검증 결과 각 항목에서 안전함이 확인되었으며 불필요한 계산을 하지 않고 효율적으로 동작을 종료하였다. 자동차 보안 분야에서 안전한 통신 환경이 되도록 설계되었음이 검증되었다.
3]과 같이 각 공격에 대해 안전하다는 결과를 출력하였으며 안전하게 마무리 되었다. 본 논문에서 제안한 인증프로토콜을 Casper/FDR 프로그램을 실행하여 보안프로토콜의 보안성을 검증한 결과[Fig. 3]와 같이 모든 보안속성에 대한 만족함이 확인되었다.
시스템에서 각 스텝별로 정상적인 프로세스로 동작했는지 확인한 결과로써 본 논문에서 제안된 프로토콜을 확인한 결과 안전한 프로세스로 동작됨을 확인하였다.
프로토콜의 보안성 확인 부분으로 제안한 프로토콜이 공격자에게 안전함을 나타낸다. 검증한 Agent간 통신과 데이터값과 세션키의 보안성이 안전한지 확인하였다.

후속연구

최근 자동차 통신시스템에서 디바이스간의 안전한 통신을 위해 뒤늦게 보안 분야에 많은 연구가 이루어지고 있다. 향후 각종 산업 분야에서 M2M 통신은 필연적으로 사용될 예정이다. 그러나 M2M 통신에서 무선으로 통신이 이루어지는 구간의 취약성을 이용하여 악의 적인 공격자의 공격에 심각한 문제가 발생할 수 있다.
자동차 보안 분야에서 안전한 통신 환경이 되도록 설계되었음이 검증되었다. 향후 군사 및 의료장비 분야에서 안전하게 통신할 수 있는 확장연구를 진행할 계획이다.

질의응답

핵심어	질문	논문에서 추출한 답변
	Casper는 무엇인가?	Casper(a Compile for the Analysis of Security Protocols)는 CSP(Communication Sequential Process) 방식으로 프로토콜을 명세하기 쉽게 개발 되어진 컴파일러이다[15]. 명세 방법은 변수타입 및 함수선언, 통신 에이전트의 초기상태, 에이전트 간의 메시지교환 순서, 검증하고자 하는 보안 속성선언, 실제 데이터타입 및 이름을 선언한다.
	자동차에 적용된 M2M은 어떤 문제를 가지고 있는가?	자동차에서도 차량내부 장치 간, 차대 차, 차와 교통시설물, 차와 주변의 환경 등에 적용되고 있다. 그러나 통신시스템의 특성상 전송구간에서 공격자의 공격에 대한 문제가 있으며 자동차의 운행, 제어계통 및 엔진제어 등에 공격자의 공격이 진행되면 안전에 심각한 문제가 발생하게 된다. 따라서 디바이스 간 보안통신에 대한 연구가 활발히 진행되고 있다.
	M2M은 어떻게 운영되는 시스템인가?	M2M은 기상, 환경, 물류, 국방, 농.축산 등에서 사용하기 시작하여 장비들이 자동으로 상황에 맞추어 통신을 하고 상황에 맞는 동작을 함으로써 운영해가는 시스템이다. 자동차에서도 차량내부 장치 간, 차대 차, 차와 교통시설물, 차와 주변의 환경 등에 적용되고 있다.

참고문헌 (17)

V. Galetic et al., Basic principles of Machineto-Machine communication and its impact on telecommunications industry. in Pro. of 34th International Convention on Information and Communication Technology, Electronics and Microelectronics, pp. 89-94, 2011.
G. Wu, S. Talwar, K. Johnsson, N. Himayat, and K. D. Johnson, M2M: from mobile to embedded internet. IEEE Communications Magazine, Vol. 49, No. 4, pp. 36-43, 2011.

상세보기
G. Wu, S. Talwar, K. Johnsson, N. Himayat and K.D. Johnson, M2M: From mobile to embedded internet. IEEE Communications Magazine, Vol.49, No.4, pp. 36-43, 2011.

상세보기
ETSI, Machine-to-Machine communications (M2M); M2M service requirements. TS 102 689 V1.1.2., 2011.
Huy Hoang Ngo, XianpingWu, Phu Dung Le and Bala Srinivasan, An individual and group authentication model for wireless network services. Journal of Convergence Information Technology, Vol.5, No.1, pp. 82-94, 2010.
Chen C, He D, Chan S, Bu J, Gao Y, Fan R., Lightweight and provably secure user authentication with anonymity for the global mobility network. International Journal of Communication Systems 2010; 24:347-362. DOI:10.1002/dac.1158.

상세보기
Qi X. A new authenticated key agreement for session initiation protocol. International Journal of Communication Systems 2011; 25:47-54. DOI:10.1002/dac.1286.

상세보기
You I, Lee J-H, Kim B, Ilsun Y, Jong-Hyouk L, Bonam K. caTBUA: context-aware ticket-based binding update authentication protocol for trust-enabled mobile networks. International Journal of Communication Systems 2010;23:1382-1404. DOI: 10.1002/dac.1113

상세보기
ISO 26262, Road vehicles - Functional safety, Management of functional safety & Concept phase
Aiash M, Mapp G, Lasebae A, Phan R, Loo J., A formally verified AKA protocol for vertical handover in heterogeneous environments using Casper/FDR. EURASIP Journal on Wireless Communications and Networking 2012.
ETSI, Machine to Machine Communications (M2M); M2M functional architecture. ETSI, TS 102 690, DEC, 2011.
G. Lowe. Casper: A compiler for the analysis of security protocols. User Manual and Tutorial. Version 1.12, 2009.
Formal systems (Europe) Ltd.: Failures-Divergence Refinement. FDR2 User Manual. Available from: pdf [Accessed 19 August 2011]
PRESERVE(PREparing SEcuRe VEhicle-to-X Communication Systems)Deliverable 1.1, Security Requirements of Vehicle Security Architecture. June. 2011.
Ryan P, Schneider S, Goldsmith M, Lowe G, Roscoe AW., The Modelling and Analysis of ecurity Protocols. PEARSON Ltd.: Edinburgh Gate. UK, 2010
M. S. Han, W. S. Bae, Security Verification of a Communication Authentication Protocol in Vehicular Security System. Journal of Digital Convergence, Vol. 12, No. 8, pp. 229-234, 2014.
Weis, S. et al., Security and Privacy Aspects of Low-Cost Radio Frequency Identification Systems. First International Conference on Security in Pervasive Computing, 2003.

내보내기 구분	파일저장 인쇄 메일전송
구성항목	기본정보 상세정보 관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관 관리번호, 논문명, 대등논문명, 저자 , 저널/프로시딩명, 발행기관, 발행년, 발행언어, 권, 호, 시작페이지, 끝페이지, ISBN, ISSN, 주제분야, 키워드, 초록(한글), 초록(영문), 저자(소속기관)
저장형식	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

연합인증

[국내논문] 자동차 보안시스템에서 장치간 상호인증 및 정형검증
Inter-device Mutual Authentication and Formal Verification in Vehicular Security System 원문보기

초록
AI-Helper

Abstract ▼ AI-Helper

주제어

AI 본문요약
AI-Helper

문제 정의

제안 방법

성능/효과

후속연구

질의응답

참고문헌 (17)

이 논문을 인용한 문헌

저자의 다른 논문 :

관련 콘텐츠

원문 보기

원문 URL 링크

오픈액세스(OA) 유형

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

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

연합인증

[국내논문] 자동차 보안시스템에서 장치간 상호인증 및 정형검증 Inter-device Mutual Authentication and Formal Verification in Vehicular Security System 원문보기

초록 용어보기논문에서 용어와 풀이말을 자동 추출한 결과로, 시범 서비스 중입니다. AI-Helper

Abstract ▼ AI-Helper

주제어

AI 본문요약 엑셀 다운로드 AI-Helper

문제 정의

제안 방법

성능/효과

후속연구

질의응답

참고문헌 (17)

이 논문을 인용한 문헌

저자의 다른 논문 :

이상준 (1)

관련 콘텐츠

원문 보기

원문 URL 링크

오픈액세스(OA) 유형

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

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

[국내논문] 자동차 보안시스템에서 장치간 상호인증 및 정형검증
Inter-device Mutual Authentication and Formal Verification in Vehicular Security System 원문보기

초록
AI-Helper

AI 본문요약
AI-Helper