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

2020/11/18 - [Report/Project] - [Ban Logic, AVISPA] IoV환경에서의 사용자 인증 프로토콜정형화 분석 1 이 포스트는 이전 포스트에서 이어지는 글입니다. 5. 정형화검증 결과 (1) 재전송 공격 재전송 공격 가능 여부를 확인하기 위해서 인증 메시지의 freshness를 확인해야한다. WSN프로토콜은 재전송 공격에 취약하다. 이를 보완하기 위해서는 (H1)을 만족해야하므로 SNj는 의사난수 생성기가 아닌 타임스탬프를 사용해야 한다. 타임스탬프를 공유하기 전에 SNj와 VSk는 사전에 시간 동기화가 반드시 필요하다. VSk는 인증 메시지의 타임 스탬프를 검증하기 때문에 메시지가 도청되어 재전송되더라도 공격 여부를 알 수 있다. 위와 같이 메시지를 추가할 경우 재전송 공..