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

2020/11/18 - [Report/Project] - [Ban Logic, AVISPA] IoV환경에서의 사용자 인증 프로토콜정형화 분석 1

이 포스트는 이전 포스트에서 이어지는 글입니다.

5. 정형화검증 결과

(1) 재전송 공격

재전송 공격 가능 여부를 확인하기 위해서 인증 메시지의 freshness를 확인해야한다. WSN프로토콜은 재전송 공격에 취약하다. 이를 보완하기 위해서는 (H1)을 만족해야하므로 SNj는 의사난수 생성기가 아닌 타임스탬프를 사용해야 한다. 타임스탬프를 공유하기 전에 SNj와 VSk는 사전에 시간 동기화가 반드시 필요하다. VSk는 인증 메시지의 타임 스탬프를 검증하기 때문에 메시지가 도청되어 재전송되더라도 공격 여부를 알 수 있다. 위와 같이 메시지를 추가할 경우 재전송 공격에 안전하다.

(2) 도난된 스마트카드 공격

스마트카드 획득을 통해 공격자는 {Ai,Bi,TIDi,Qi}를 알 수 있다. 스마트 카드에는 아래와 같은 정보들이 계산되어 저장되어 있다. Xi = h(IDi||KS), Ai = Xi⊕h(IDi||HPWi), Bi = h(HPWi||Xi), Ci = Xi ⊕h(TIDi||KS), and Qi = h(IDi||PWi)⊕ai. 하지만 공격자는 IDi, PWi 에 대한 정보 없이 XOR로 마스킹된 민감 정보를 볼 수 없다. 따라서 이 프로토콜은 도난된 스마트 공격으로부터 안전하다.

(3) 안전한 상호 인증

Ua가 정당한 사용자 Ui인척 하는 가장 공격을 수행하려고 할 때, Ua는 반드시 {MTS,M1,M2,CIDi,TIDi}를 전송하고 받은 {MST,M5,n,m}에 대해 {M6}를 성공적으로 응답해야 한다. 그러나 Ua는 IDi에 대한 정보를 알 수 없으므로 Xi를 알 수 없다. 또한 Ui와 SNj가 공유하는 비밀인 Ks도 알 수 없어 유효한 메시지를 생성할 수 없다.

 

 

6. 개선된 프로토콜 제안

본 장에서는 정형화 검증 단계에서 식별한 문제를 개선하여 새로운 프로토콜을 제안한다.

Ban Logic 검증에서 G3, G4를 이끌어내기 위해서 H1를 적용해야 한다. H1을 Assumption으로 바꾸기 위해서는 메시지의 freshness 확인이 필요하다. 따라서 Timestamp를 메시지에 포함시켜 전송하여 수신측에서 time window 범위를 확인함으로써 freshness 검증을 수행하였다. 개선된 프로토콜에 대한 반로직 검증은 아래와 같다.

(D6) ~ (D10)을 통해 (G3), (G4)를 만족한다. 기존 프로토콜과는 다르게 ts(timestamp)를 추가함으로써 freshness를 검증할 수 있다. 그러므로 (G3), (G4)를 이끌어낼 수 있다.

  악의적인 사용자(Ua)가 메시지를 무한으로 전송할 수 있을 때 SNj나 VSk에서 새롭게 생성해서 보낸 메시지인지 검증과정이 없기 때문에 재전송 공격에 취약하다. 기존의 프로토콜은 SNj에서 VSk로 {MSV,M3,M4} 메시지를 보낼 때 받는 VSk에서는 랜덤 넘버인 RSj의 freshness를 알 수 없다. 무한으로 메시지 전송이 가능한 환경에서 검증 없이 통신이 유지될 때 트래픽 과부하가 발생하여 망의 가용성이 저하된다. 따라서 기존의 메시지 {MSV,M3,M4}에서 Time Stamp를 추가하여 전송한다.

7. 결론

본 포스트에서는 IoV 환경에서 사용되는 WSN 네트워크에 사용되는 보안 프로토콜의 취약점을 BAN Logic과 AVISPA를 사용해 정형화 검증을 수행하였다. 검증 과정에서 식별된 재전송 공격에 대한 위협을 Timestamp를 추가하여 개선하였다. 이를 새로 BAN논리를 이용하여 검증을 수행함으로써 안정성 여부를 확인하였다.

---

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.