Dolev-Yao 공격자 모델과 기호 암호학

1983년 Danny Dolev와 Andrew Yao가 제안한 Dolev-Yao 모델은 기호 프로토콜 분석에서 사용하는 표준 공격자 모델입니다. 공격자는 전체 네트워크를 통제합니다.

Dolev-Yao 공격자는 다음을 수행할 수 있습니다. 모든 메시지를 가로채고, 메시지를 저장하고, 이전 메시지를 재전송하고, 알고 있는 구성 요소로 새 메시지를 위조할 수 있습니다. 그러나 기본 암호화 요소를 깨뜨릴 수는 없습니다.

기호 모델에서 암호화는 완벽한 블랙박스입니다. 공격자는 키 없이는 복호화할 수 없고, 큰 수를 인수분해할 수 없으며, 서명을 위조할 수 없습니다. 이 가정은 분석을 단순하게 만들지만 구현 수준의 공격을 놓칠 수 있습니다.

메시지는 enc(k, m), sig(sk, m), hash(m), pair(a, b)와 같은 항으로 모델링됩니다. 공격자는 특정 항을 알고 있으며, 정의된 규칙(추론 규칙)을 사용해 새로운 항을 도출합니다.

공격자의 지식은 추론에 대해 닫혀 있습니다. 공격자가 enc(k,m)과 k를 알고 있다면 m을 도출할 수 있습니다. pair(a,b)를 알고 있다면 a와 b를 도출할 수 있습니다. 초기 지식의 폐쇄 = 공격자가 학습할 수 있는 모든 것입니다.

프로토콜 보안은 다음과 같이 표현됩니다. "도달 가능한 어떤 상태에서도 공격자의 지식에 비밀 s가 포함되지 않습니다." 기밀성 = 도달 가능성입니다. 인증 = 특정한 잘못된 실행 추적 패턴이 존재하지 않는 것입니다.

양자 프로토콜: A→B: {Na, A}_{K_B}; B→A: {Na, Nb}_{K_A}; A→B: {Nb}_{K_B}. 항 대수에서는 Alice가 enc(pubkey_B, pair(Na, A))를 보냅니다. 실행 후 Na를 아는 주체가 B뿐인지 검증합니다.

적용된 파이 계산법(Abadi와 Fournet, 2001)은 프로토콜을 모델링하기 위한 과정 대수입니다. 과정은 채널을 통해 통신하며, 공격자는 공개 채널을 제어합니다. ProVerif와 Tamarin은 이 형식 체계를 사용합니다.

Dolev-Yao 모델에서 안전한 프로토콜도 암호학적 구현이 취약하면 계산적으로 안전하지 않을 수 있습니다. 계산적 건전성 정리(Cortier 등)는 특정 기본 요소 클래스에 대해 이 간극을 연결합니다.

Dolev-Yao는 대수적 성질(예: XOR의 교환 법칙), 부채널 공격, 구현 버그 또는 확률적 실패를 모델링할 수 없습니다. 등식 이론 모델과 같은 확장은 일부 대수적 성질을 처리합니다.

Dolev-Yao 공격자가 갖지 못하는 능력(NOT)은 무엇입니까?

Dolev-Yao는 공격자에게 네트워크를 완전히 제어할 수 있는 권한을 부여하지만 완벽한 암호를 가정합니다. 메시지는 대수의 항이며, 보안은 도달 가능성 속성입니다. 적용된 파이 계산법은 형식 언어를 제공합니다. 한계: 대수적 관계, 부채널 또는 구현 버그를 모델링할 수 없습니다.