🛡️ [클래식] On the Security of Public Key Protocols — '사칭·변조하는 능동적 공격자'를 정면으로 다룬 최초의 형식 모델: Dolev–Yao 모델의 탄생 (1983)

논문 정보

연구 배경 — "공개키는 도청은 막지만, 사칭은 막지 못한다"

1980년대 초, 공개키 암호는 수동적 도청자(passive eavesdropper)에게는 결정적인 무기로 여겨졌다. 회선을 도청해 암호문을 얻어도 개인키 없이는 복호화할 수 없으니 안전하다는 것이다.

논문은 이 안도감을 첫 문단에서 정면으로 부순다. 문제는 능동적 사보퇴르(active saboteur)다. 이 공격자는 도청만 하지 않는다 — 다른 사용자를 사칭하고(impersonate), 전송 중인 메시지를 가로채고 바꿔치기하며, 자기 키로 재암호화해 다시 흘려보낸다. 논문이 던진 질문은 이랬다. "공개키가 완벽하다고 가정해도, 프로토콜 자체가 잘못 설계되면 안전하지 않다. 그렇다면 프로토콜 안전성을 어떻게 '정확히' 논할 수 있는가?"

논문은 이 질문에 답하기 위해 여러 개의 수학적 모델을 세우고, 그 안에서 안전성을 판정하는 알고리즘과 특성화(characterization)를 제시했다. 그것이 오늘날 Dolev–Yao 모델로 불리는 상징적 프로토콜 분석의 출발점이다.

논문이 든 첫 예시 — '이름을 암호문 밖에 두면' 프로토콜이 깨진다

논문은 메시지를 세 개의 필드로 정의한다: 발신자 이름, 텍스트(암호문), 수신자 이름. 그리고 도입부에 지금은 교과서가 된 프로토콜을 하나 제시한다. A가 B에게 평문 M을 보내는 방식이다.

a) A → B : (A, E_B(M), B)
b) B → A : (B, E_A(M), A)

얼핏 완벽해 보인다. M은 B의 키로, 다시 A의 키로 감싸져 있다. 그런데 논문은 "이 프로토콜은 놀랍게도(surprisingly) 깨진다"며 네 단계 공격을 제시한다.

• ① 가로채기: 사보퇴르 Z가 1단계에서 A→B 메시지 (A, E_B(M), B)를 가로챈다. E_B(M) 부분을 확보한다.
• ② 사칭: Z가 자신이 발신자라고 주장하며 B에게 (Z, E_B(M), B)를 보낸다. B의 공개키로 암호화돼 있으니 B는 의심 없이 받아들인다.
• ③ 되돌아오는 답장: B는 프로토콜대로 응답한다 — (B, E_Z(M), Z). 즉 방금 받은 평문 M을 Z의 공개키로 암호화해 Z에게 보내준다.
• ④ 복호화: Z는 자신의 개인키로 E_Z(M)을 열어 평문 M을 그대로 얻는다.

근본 원인은 수신자 이름이 암호문 안에 들어 있지 않다는 점이다. B는 자기가 받은 E_B(M)이 A가 보낸 것인지 Z가 보낸 것인지 구분할 수 없다. 이는 훗날 "이름은 반드시 암호문 안에 함께 서명·암호화해야 한다(name-stamp)"는 원칙으로 자리 잡는다 — 그리고 논문은 바로 그 원칙을 형식 모델로 증명하러 간다.

두 가지 모델 — Cascade Protocols와 Name-Stamp Protocols

논문은 먼저 '완벽한 공개키 시스템(perfect public key system)'이라는 명시적 가정을 깐다. 이 가정 목록 자체가 훗날 모든 상징적 모델의 표준이 된다.

• 가정 a) 사용되는 일방향 함수는 깨지지 않는다(unbreakable).
• 가정 b) 공개 디렉터리(public directory)는 안전하고 변조될 수 없다.
• 가정 c) 모든 사용자가 모든 사용자의 공개 암호화 함수 E_X에 접근할 수 있다.
• 가정 d) 복호화 함수 D_X는 사용자 X만 알고 있다.

이 위에서 논문은 두 부류의 프로토콜을 정의한다.

• ① Cascade Protocols(연쇄 프로토콜): 사용자가 암호화·복호화 연산자를 조합해 메시지를 만든다. 여러 겹을 겹칠 수 있다. 기본 성질은 E_X D_X = D_X E_X = 1(항등함수) — 즉 암호화 후 자기 키로 복호화하면 원문으로 돌아온다.
• ② Name-Stamp Protocols(이름 도장 프로토콜): 사용자가 이름을 평문과 함께 암호화해 붙이고(append), 지우고(delete), 검사(check)할 수 있다. 암호 계층이 여러 겹 들어갈 수 있다 — 위 도입 예시의 '교정판'이 이 부류다.

핵심 결과 — 안전성은 '증명'할 수 있고, 때로는 '자동 판정'할 수 있다

논문의 가장 큰 공헌은 개념 정리만이 아니라 구체적인 알고리즘과 정리다. 논문 자체 요약이 밝히는 결과는 이렇다.

• 연쇄 프로토콜의 안전성 특성화: 사보퇴르가 메시지를 변조·사칭해 평문에 도달할 수 있는지를 사보퇴르 지식의 닫힘(closure) C(·) 으로 형식화하고, 연쇄 프로토콜이 안전할 필요충분조건을 제시한다. 예컨대 안전한 프로토콜은 메시지 흐름이 균형(balanced) 조건을 만족해야 한다 — 그래야 사보퇴르가 암호 연산자를 조합해 원문을 벗겨낼 수 없다.
• 이름 도장 프로토콜 판정 알고리즘(§III): 주어진 이름 도장 프로토콜이 안전한지 다항시간에 결정하는 알고리즘을 제시한다. 안전성은 더 이상 '전문가의 직관'이 아니라 계산 가능한 문제가 되었다.
• 일반 문제의 결정 불가능성 vs 특수 클래스의 다항시간: 논문이 다루는 확장 단어 문제(extended word problem)는 type-0 언어 멤버십 문제를 부분 사례로 포함하므로 일반적으로는 결정 불가능(undecidable)하다는 것이 알려져 있었다. 논문은 이 지점에서 물러서지 않고, 특정 조건을 만족하는 입력 클래스에서는 다항시간에 풀린다는 것을 보였다 — 취소 규칙(cancellation rule, a₁a₂ → λ)이 있는 확장 단어 문제를 약 O(n⁷) 에 푸는 알고리즘(Theorem 4)이 그 핵심이다.
• '조급한 사보퇴르(impatient saboteur)' 확장(§IV): 지금까지는 사보퇴르가 다른 사용자의 대화 개시를 기다려야 했지만, 논문은 사보퇴르가 먼저 대화를 시작할 수 있는 더 강한 모델로 결과를 확장한다. 정상 사용자 사이의 전송 형태를 제약해(예: 상대 이름을 확인하지 못하면 전송이 진행되지 않음) 안전성을 재특성화한다.

공격자 모델 — "공격자가 메시지를 나른다(the attacker carries the message)"

이 논문이 후대에 Dolev–Yao 모델이라는 이름으로 각인된 이유는, 공격자 능력을 과감할 만큼 강력하게 그리고 수학적으로 다룰 수 있게 정의했기 때문이다.

• 네트워크 전권 통제: 공격자는 메시지를 도청(overhear)·가로채기(intercept)·삭제·재전송·합성(synthesize)할 수 있고, 사실상 네트워크 그 자체다. 문헌의 표현대로 "공격자가 메시지를 나른다."
• 정당한 참여자로서의 사칭: 공격자는 자기 키 쌍을 갖고 있으며 스스로 세션을 개시하고 어느 사용자와도 대화를 시도할 수 있다. 모든 공개키를 안다.
• 지식의 재사용·위조: 이미 흘러간 메시지를 저장했다가, 자기가 아는 키로 암호화·복호화하며 후속 메시지를 위조할 수 있다.
• 단, 암호는 완벽한 블랙박스: 암호문 E_x(M)은 M에 대해 아무 정보도 노출하지 않는다. 공격자는 암호문의 비트 표현을 조작하거나 키를 추측할 수 없다 — 암호는 이상적 연산자로 취급된다.

즉 '무엇을 할 수 있는가'는 최대한 강하게, '암호 자체를 깨는 것'은 가정으로 배제한 것이다. 이 비대칭이 메시지 흐름의 논리(logic of message flow) 만을 다루는 상징적 분석을 가능하게 만들었다.

왜 지금도 인용되는가 — 5,842회가 향하는 곳

• 프로토콜 검증 도구의 공통 뿌리: ProVerif, Tamarin, AVISPA, Scyther, CPSA 같은 자동 검증 도구는 모두 Dolev–Yao식 상징적 공격자를 전제로 동작한다. TLS 1.3, SSH, WPA, 시그널 프로토콜, 5G 인증 절차의 상징적 검증이 이 모델 위에서 이뤄졌다.
• '깨졌다'를 보이는 데 특히 강력: 상징적 모델은 프로토콜이 안전함을 증명하는 데는 한계가 있어도, 깨졌음을 보이는 데는 탁월하다 — 공격 트레이스(반례)를 구체적으로 뽑아낸다. Needham–Schroeder 공개키 프로토콜의 재전송 공격(Lowe, 1995)은 이 틀 위에서 발견된 대표 사례다.
• 상징적 모델의 '계산적 건전성'이라는 후속 학문을 낳았다: 대수적 상징 모델은 실제 비트 수준 암호보다 단순하다. 그래서 "상징적 안전 ⇒ 계산적 안전"을 증명하는 computational soundness 연구가 이어졌다 — Abadi–Rogaway(2000)를 시작으로 Micciancio–Warinschi, Backes–Pfitzmann–Waidner 등이 그 계보다.
• 한계도 잘 알려져 있다: 패딩 오라클(Bleichenbacher)·타이밍·전력 분석처럼 암호 구현의 비트 수준 결함에 의존하는 공격은 Dolev–Yao 대수로 표현되지 않는다. 재밌는 대조다 — 2026-09-11에 다룬 Rowhammer, 2026-08-31의 Kocher 타이밍 공격은 정확히 이 모델의 사각지대에서 나온 공격들이다.
• 교육적 가치: "이름을 암호문 안에 넣어라", "상대와 세션을 묶어라(채널 바인딩)" 같은 오늘날의 프로토콜 설계 원칙은 대부분 이 논문의 형식화와 그 반례들에서 나왔다.

출처

• 정식판 (IEEE ToIT 1983, DOI): doi.org/10.1109/TIT.1983.1056650
• 저자 제공 PDF 전문 (Danny Dolev, 히브리대학교): cs.huji.ac.il/~dolev/pubs/dolev-yao-ieee-01056650.pdf
• FOCS 1981 예비판 (DOI): doi.org/10.1109/SFCS.1981.32
• 함께 읽기 — Dolev–Yao 모델 개요: Wikipedia: Dolev–Yao model
• 함께 읽기 — 이전 게시물: 2026-09-11 Rowhammer (DRAM 교란) · 2026-08-31 Kocher Timing Attacks (사이드채널의 시작) · 2026-09-14 Security Problems in the TCP/IP Protocol Suite (Bellovin, 1989)