[Ban Logic, AVISPA] IoV환경에서의 사용자 인증 프로토콜정형화 분석 1

Summary

IoV(Internet of Vehicle) 기술이 등장함에 따라 WSN(Wireless Sensor Networks)기술이 함께 등장하였다. 인터넷의 발전은 운전자들의 편안한 운전을 위해 다양한 정보에 접근이 가능하도록 한다. 예를 들어 교통 흐름, 응급 상황, 차량 사고 정보들이 이에 해당한다. 하지만 운전자와 도로 관리자 사이의 통신은 공개된 채널을 사용하기 때문에 다양하고 많은 보안 위협들이 존재한다. 그러므로 안전한 상호 인증과 통신의 암호화가 필수적이다. Sima Arasteh 외 2명의 논문[1]에서는 2017년에 차량을 위한 안전한 WSN 차량 상호인증 보안 프로토콜을 제안하였다. 본 논문은 제안된 WSN 차량 상호인증 보안 프로토콜을 분석하고 안전성을 BAN 논리와 avispa를 통해 검증한다.

1. 서론

1. IoV

IoV(Internet of Vehicle)은 자동차에 정보통신 기술을 융합해 차량 간 통신을 수행하고 지능적 관계를 형성하는 것을 의미한다. 차량의 운행에 필요한 교통신호, 차량 사고와 속도 정보를 운전자가 알 수 있게 한다. 이러한 정보를 제공하기 위해 차량의 센서들은 차량 주변의 정보를 수집하여 실시간으로 서버로 전송한다. 하지만 공개된 채널의 통신을 사용하기 때문에 악의적인 사용자가 쉽게 조작한 데이터를 전송할 수 있다는 취약점이 존재한다. 그러므로 IoV 프로토콜을 사용하기 위해서는 서버와 사용자 간의 안전한 인증 과정이 필수적이다.

2. 위협모델

제안된 프로토콜의 안전성을 분석하고 보안성을 평가하기 위해 널리 사용되는 Dolev-Yao(DY) 위협 모델을 소개한다. DY위협 모델에서는 공격자를 다음과 같이 정의한다.

- 공격자는 공개 채널에서 전송되는 데이터를 도청, 조작하거나 삽입, 삭제할 수 있다.

- 공격자는 분실, 도난된 스마트카드로부터 데이터를 추출해낼 수 있다.

- 공격자는 개인화, 추적, 재전송 등 공격을 하기 위해 다양한 작업을 수행할 수 있다.

본 글의 구성은 다음과 같다. 2장에서는 WSN 프로토콜을 소개하고 분석한다. 3장에서는 BAN 논리를 이용하여 프로토콜에 대한 정형화 분석을 실시하고, 4장에서는 AVISPA를 이용하여 검증 결과를 서술한다. 7장을 끝으로 결론을 맺는다.

2. WSN 프로토콜 분석

본 장에서는 WSN 프로토콜의 사용자 등록, 인증하는 단계를 소개한다. 이 프로토콜은 사용자 등록단계와 인증단계로 구성된다.

1. 등록단계

운전자가 센서를 배치하려고 할 때, 등록 관리자(RA; Registration Authority)는 차량 센서를 네트워크에 등록한다. 추가적으로 RA는 차량 번호, 엔진, 배터리, 보험 기록 등 정보를 저장한다.

만약 새로운 사용자 Ui가 등록하려고 할때, 등록 요청 메시지를 sink node인 SNj로 먼저 전송해야 한다. 등록 과정의 통신은 아래와 같다.

[그림 1] 등록 단계

Step 1. Ui는 계정정보인 IDi와 PWi, 그리고 랜덤값 ai를 생성한다. Ui는 HPWi=h(PWi||ai)를 계산한다. 그리고 Ui는 {IDi,HPWi} 결과를 SNj에게 보안 채널로 전송한다.

Step 2. Ui에게서 등록 요청 메시지를 수신하면, SNi는 Ui에 대한 고유 식별 정보 TIDi를 생성한다. 그리고 X, Ai, Bi, Ci를 계산한다. 그리고 SNj는 스마트카드(smartcard)에 {Ai, Bi, TIDi}를 저장하고 Ui에게 발급해 준다. 마지막으로 SNj는 {TIDi, Ci}를 데이터베이스에 저장한다.

Step 3. SNj가 전송한 스마트카드로부터 Ui는 Qi를 계산하여 스마트카드에 저장한다. 결과적으로 SNj는 스마트카드에 {Ai, Bi, TIDi, Ci}를 저장하게 된다.

2. 인증단계

[그림 2] 인증단계

Step 1. Ui는 스마트카드에게 아이디 IDi와 패스워드 PWi를 입력한다. 그러면 Ui는 ai=h(IDi||PWi)⊕Qi, HPWi=h(PWi||ai), Xi=h(IDi||HPWi)⊕Ai, B* i=h(HPWi||Xi)를 계산하고 B*i가 등록과정에서 생성한 Bi와 일치여부를 확인한다. 일치한다면 U는 랜덤한 값인 RUi를 생성하고 M1=RUi⊕Xi, M2=IDk⊕h(Xi||RUi), CIDi=IDi⊕h(TIDi||Xi||RUi), MTS=h(IDi||Xi||RUi)를 계산한다. 그리고 Ui는 로그인 요청 메시지인 {MTS,M1,M2,CIDi,TIDi}를 SNj에게 전송한다.

Step 2. Ui로부터 로그인 요청 메시지를 받으면 SNj는 일치하는 Ci와 TIDi가 있는지 여부를 검색한다. 후에 Xi=Ci⊕h(TIDi||KS),RUi=M1⊕Xi,IDi=CIDi ⊕h(TIDi||Xi||RUi),IDk=M2⊕h(Xi||RUi), and M*TS=h(IDi||Xi||RUi)를 계산하고 MTS 와 일치 여부를 확인한다. 만약 일치한다면, SNj은 랜덤한 값인 RSj 를 생성하고 Xk=h(IDk||Ks),MSV=h(IDk||IDj||Xk||RSj), M3=RSj⊕h(IDj||Xk),and M4=IDk⊕IDj을 계산한다. 또한 SNj는 인증 요청 메시지인 {MSV,M3,M4}를 VSk에게 공개채널로 보낸다.

Step3. {MSV,M3,M4}메시지를 수신하면 VSk는 IDj=M4⊕IDk를 계산하고 RA로부터 Xk를 수신 받는다. 그리고 VSk는 RSj=M3⊕h(IDj||Xk)와 M*SV=h(IDk||IDj||Xk||RSj)를 계산한다. 그리고 MSV와 일치 여부를 확인한다. 만약 일치하면, VSk는 랜덤한 값인 RVk를 생성하고 vi=h(IDk||RSj||RVk), MVS=h(Xk||RSj||vi), t=RSj ⊕RVk를 계산한다. 마지막으로, VSk는 SNj에게 {MVS,t}를 전송한다.

Step4. VSk로부터 메시지 {MSV,t}를 수신하면, SNj는 RVk=t⊕RSj, vi=h(IDk||RSj||RVk), M*VS=h(Xk||RSj||vi)를 계산한다. 그리고, SNj 는 생성한 M*VS와 수신한 MVS의 일치 여부를 확인한다. 만약 일치한다면, SNj는 n=RSj⊕RUi, m=RVk⊕RUi를 계산한다. 그리고 SNj는 새로운 무작위 값인 TIDinew를 생성하고 M5=TIDinew⊕h(RSj||RVk), MST=h(RUi||RSj||RVk||IDk||IDi)를 계산한다. SNj 는 Ui에게 메시지 {MST,M5,n,m}를 전송한다.

Step5. {Msv, M5, n, m}메시지를 수신하면 Ui는 RSj=n⊕RUi, RVk=m⊕RUi, TIDinew=M5⊕h(RSj||RVk), M*ST=h(RUi||RSj||RVk||IDk||IDi)를 계산한다. 그리고 Ui를 M*st=?Mst가 같은지 아닌지 확인하고, 같으면 Ui는 TIDi를 TIDinew로 갱신한다. 마지막으로 Ui는 M6=h(IDi||RUi||RSj)를 만들고 SNj한테 M6를 보낸다.

Step6. Ui로부터 {M6}를 받은 후에 SNj가 M*6=h(IDi||RUi||RSj), C*i=Xi⊕h(TIDinew||Ks)를 계산한다. 그리고 SNj는 M*6=?M6가 같은지 확인하고, 같으면 SNj는 {TIDi, Ci}를 {TIDinew, C*i}로 바꾼다.

 

 

3. WSN 프로토콜 BAN 논리 검증

BAN 논리는 Michael Burrows, Martin Abadi와 Roger Needham에 의해서 제안된 인증 프로토콜을 정형화된 방식으로 기술하고 분석하는 방법이다.

본 장에서는 2장에서 분석한 WSN의 인증 프로토콜을 BAN 논리로 검증하였다.

검증 중에 필요한 규칙 중 MM은 Message Meaning Rule, NV은 Nonce Verification Rule, JR 은 Jurisdiction Rule, FR은 Freshness Rule, BC는 Belief Conjunction Rule을 의미한다.

[표 1] BAN 논리의 규칙, 표현

 

(D6) ~ (D10)을 통해 (G3), (G4)를 만족한다. 그러나 (D8)에서 Freshness Rule을 적용할 때 VSk은 SNj가 보낸 것 중에 최신의 값이라고 믿을 수 있는 메시지가 없다. 그에 따라 (H1)을 가정함으로써 (G3), (G4)를 만족한다. 그리고 (D16) ~ (D20)를 통해 (G7), (G8)을 만족한다.

4. WSN 프로토콜 AVISPA 검증

  이 장에서는 자동화된 정형화 검증 도구인 AVISPA(Internet Security Protocols and Applications) 가상 도구를 사용하여 프로토콜에 대한 공식적인 보안 검증을 수행한다. 이 도구를 사용한 공식적인 보안 검증은 많은 관심을 받았으며 다양한 인증 프로토콜이 재전송 및 중간자 공격으로부터 안전하다는 것을 입증하기 위해 수많은 연구에 사용되어 왔다[5,6,7].

  AVISPA의 경우, 보안 프로토콜은 반드시 HLPSL(High Level Protocols Specification Language)을 사용하여 구현되어야 한다. 보안 프로토콜의 HLPSL 규격은 HLPSLIF 변환기에 의해 중간 형식(IF)로 변환된다. 마지막으로 On-the-fly Model-Checker(OFMC), CL 기반 공격 검색기(AtSe) 또는 Tree Automata 기반 Protocol Analyzer(TA4SP)로 출력 형식(OF)로 변환된다[6].

HLPSL에 따르면 제안된 프로토콜은 세 개의 엔티티가 있는데, 이를 역할이라고 한다. UA(User Agent)는 사용자를 나타내고, SN(Sink Node)는 싱크노드를 나타내고, VS(Vehicle Sense)는 차량 센서를 나타낸다. 세션(Session)과 환경(Environment)도 [그림 6]에 보안 목표를 포함하고 있다. U의 역할 사양은 [그림 3]에 나타나 있으며 자세한 내용은 다음과 같다.

[그림 3] User에 대한 Role 정의

[그림 5] vehiclesense에 대한 Role정의

[그림 6] Session과 Environment 정의

  [그림 7]와 [그림 8]는 ATSE와 OFMC를 백엔드 모듈로 사용한 프로토콜 AVISPA 검증 결과이다. AVISPA는 다중 세션 연결과 엔티티 검증을 수행하여 프로토콜을 실행할 수 있는지 확인한다. 또한 OFMC와 CL-AtSe 백엔드에서는 제안된 프로토콜이 DY모델 확인을 위한 중간자 공격(MITM)에 대해 안전한지 여부를 확인한다. OFMC 백엔드는 146개 노드를 방문할 수 있는 17.34초의 검색 시간을 가지며, CL-AtS 백엔드는 0.41초의 변환 시간으로 두 개의 상태를 분석한다. 재전송 공격과 Dolev-Yao 모델 확인이 성공적으로 수행되기 때문에 프로토콜은 재생 및 중간 공격으로부터 안전하다.

[그림 7] ATSE 분석결과 / [그림 8] OFMC 분석결과

위와 같은 정형화 검증을 통해 문제점을 식별하였고 다음 포스트에서 타임스탬프를 이용해 문제점을 개선한 알고리즘을 다시 설계하고 정형화 검증을 해본다.

---

References

[1] Sima Arasteh, Maede Ashouri-Talouki, Seyed Farhad Aghili. "Lightweight and Secure Authentication Protocol for the Internet of Things in Vehicular Systems". International ISC Conference on Information Security and Cryptography. 2014.

[2] 김도환, 정우진, 정건우, 유일선. Lee와 Choi가 제안한 ‘RFID 환경을 위한 태그-리더’ 상호 인증 프로토콜 검증. 정보보호학회 동계학술대회. 2016.

[3] Chatterjee, K.; De, A.; Gupta, D. A secure and efficient authentication protocol in wireless sensor network. Wirel. Pers. Commun. 2015, 81, 17–37.

[4] Kim, J.; Lee, D.; Jeon, D.; Lee, Y.; Won, D. Security anaylsis and improvements two-factor mutual authentication with key agreement in wireless sensor networks. Sensors 2014, 14, 6443–6462.

[5] FIPS PUB 180-4: Secure Hash Standard (SHS). Available online: https://nvlpubs.nist.gov/nistpubs/FIPS/ NIST.FIPS.180-4.pdf (accessd on 23 July 2018).

[6] AVISPA. Automated Validation of Internet Security Protocols and Applications. Available online: http://www.avispa-project.org/ (accessed on 4 July 2018).

[7] SPAN: A Security Protocol Animator for AVISPA. Available online: http://www.avispa-project.org/ (accessed on 4 July 2018).

[8] Wessels, Jan, and CMG FINANCE BV. "Application of BAN-logic." CMG FINANCE BV 19 (2001): 1-23.

[9] Syverson, Paul. "The use of logic in the analysis of cryptographic protocols." IEEE, 1991.