Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

기술 요약: 유한 변형 속성을 넘어: 심볼릭 디피-헬먼(Diffie-Hellman) 그룹 모델의 확장

문제 정의
디피-헬먼(DH) 그룹은 현대 암호 프로토콜의 기초가 되지만, 최첨단 심볼릭 프로토콜 검증기(Tamarin, Proverif, Maude-NPA 등)는 이들의 대수적 성질을 완전히 지원하지 못한다. 이러한 도구들은 지수의 거듭제곱과 곱셈은 모델링할 수 있지만, 지수의 덧셈에 해당하는 그룹 원소 간의 곱셈은 일반적으로 모델링할 수 없다. 이러한 한계는 결합 법칙, 결합성 및 교환성을 포함하는 풀 DH 그룹을 기술하는 등식 이론이 결정 불가능(undecidable)하고 무한한(infinitary) 유니피케이션(unification) 문제를 야기하기 때문이다. 결과적으로, 기존 도구들은 공격자나 정직한 당사자가 지수의 전체 필드 구조를 활용하여 합성된 그룹 원소를 구성하는 프로토콜(예: ElGamal 암호화 또는 MQV 키 교환)에 대해 추론할 수 없다.

방법론
저자들은 풀 DH 그룹 구조를 사용하는 프로토콜의 보안 속성을 검증하기 위한 준결정 절차(semi-decision procedure)를 제안한다. 이 접근 방식은 심볼릭 추론과 대수적 방법을 통합하며, Tamarin 프로버의 확장 기능으로 구현되었다.

1. 이론적 기초: 본 연구는 결합 법칙과 교환 법칙(AC)을 고려하여 필드를 근사하는 수렴하는 리라이트 시스템($\to_{DH}$)을 제안한 Dougherty와 Guttman의 리라이트 시스템을 기반으로 한다. 이 시스템은 항(term)의 노멀 폼(normal form)을 정의할 수 있게 한다.
2. 비취소 가정 (Non-Cancellation Assumption): 이 접근 방식은 두 가지 주요 조건에 의존한다.
   • C1: 모든 그룹 원소는 공통의 생성자를 가진 단일 고정 그룹에 속한다.
   • C2 (비취소): 보안 속성은 서브텀(subterm)들이 서로 상쇄되지 않는(즉, 항등원 1 또는 0으로 축소되지 않는) 항들을 포함한다. 이 조건이 실패할 경우, 도구는 여전히 유효한 공격을 찾아낼 수 있지만, 보안 증명을 위해서는 특정 항들이 상쇄되지 않는다는 수동 검증이 필요하다.
3. 하이브리드 제약 조건 해결 (Hybrid Constraint Solving): 핵심 혁신은 DH 항에 대한 직접적인 유니피케이션을 피하는 수정된 제약 조건 해결 알고리즘이다. 대신, 다음의 2단계 과정을 채택한다.
   • 심볼릭 유니피케이션 (단순화된 이론): 알고리즘은 먼저 그룹 곱셈 연산자를 제외한 단순화된 등식 이론($\varepsilon_{simp}$) 내에서 항들을 유니피케이션한다. 이를 통해 Tamarin의 기존 유니피케이션 알고리즘을 사용하여 루트 항(root terms)을 매칭할 수 있다.
   • 대수적 재구성: 루트 항이 매칭되면, 알고리즘은 심볼릭 항을 대수적 객체(필드 위의 다항식)로 해석한다. 지수를 "유출된(leaked)" 것(공격자가 알고 있는 것)과 "비밀(secret)"인 것으로 분류한다. 이후 가우스 소거법(또는 비선형 사례의 경우 Buchberger 알고리즘)을 사용하여, 비밀 지수들이 유출된 지수들과 결합하여 대상 항을 재구성할 수 있는지 여부를 해결한다.
4. 지표 함수 (Indicator Function): 항이 연역 가능한지 결정하기 위해, 저자들은 항을 구성하는 데 필요한 최소한의 비밀 구성 요소를 식별하는 "지표" 함수를 정의한다. 만약 어떤 지표라도 공격자의 지식으로부터 재구성될 수 없다면, 해당 항은 연역 불가능한 것으로 간주된다.
5. 공격자 모델링: 이 확장은 모든 DH 연산자를 적용할 수 있는 능동적 Dolev-Yao 공격자를 지원한다. 제약 조건 해결기는 다항식 해석으로부터 도출된 선형 방정식을 만족할 수 있는지 확인하여 공격자의 연득을 처리한다.

주요 기여

• 풀 DH 이론을 위한 최초의 자동화된 도구: 본 연구는 합성된 디피-헬먼 그룹 원소를 포함하여, 그룹 원소 간의 곱셈을 포함한 풀 디피-헬먼 그룹 구조를 모델링하고 추론할 수 있는 자동화된 검증 도구의 첫 번째 구현을 제시한다.
• 건전성 및 완전성 (Soundness and Completeness): 저자들은 확장된 제약 조건 해결 관계가 (비취소 가정 하에) 건전하고 완전함을 증명한다. 만약 Tamarin이 공격을 찾는다면 그것은 유효한 실행이며, 만약 보안을 증명한다면 제한된 범위 내에서 위반하는 실행은 존재하지 않는다.
• Tamarin과의 통합: 이 접근 방식은 Tamarin의 제약 조건 해결 알고리즘을 수정하여, DH 정렬 항에 대한 표준 유니피케이션 규칙을 대수적 해결 단계로 대체하는 새로운 규칙들($C@, C_{Prem}, C=, C_{var}$)을 추가함으로써 구현되었다.
• 혼합 이론 처리: 이 방법은 풀 DH 이론을 다른 사용자 정의 등식 이론(예: 대칭 암호화, 쌍/pairs)과 결 combining할 수 있도록 지원한다. 이는 결합된 항들을 "클리닝(cleaning)"하는 과정, 즉 유니피케이션을 위해 DH 서브텀을 새로운 변수로 교체한 후 대수적 해결을 위해 DH 제약 조건을 다시 도입하는 과정을 거친다.

결과 및 사례 연구
저자들은 다음과 같은 프로토콜에 대해 구현을 평가하였다.

• ElGamal 암호화: 이 도구는 ElGamal 암호화 방식의 실행 가능성과 비밀성을 성공적으로 증명하였다. 특히, 이는 심볼릭 모델에서 풀 DH 지원을 갖춘 상태로 ElGamal이 자동으로 검증된 첫 사례이다. 또한, 개시자(initiator)가 인증되지 않았을 때의 비밀성 결여를 정확하게 식별하였다.
• MQV 키 교환: 이 도구는 MQV 프로토콜을 분석하는 데 사용되었다. 이 도구는 합성된 그룹 원소를 포함하는 복잡한 공격을 찾아내는 능력을 입증하며, Kaliski가 알려진 "알려지지 않은 키 공유(unknown key-share)" 공격을 성공적으로 재발견하였다.
• 벤치마크 평가: 이 확장은 제한된 DH 이론을 사용했던 20개의 기존 Tamarin 모델(WireGuard 및 다양한 키 교환 프로토콜 포함)에 대해 테스트되었다. 결과에 따르면, 이 확장은 해당 프로토콜들에 대해 제한된 이론과 동일한 보안 판정을 내렸으나, 확장된 탐색 공간의 복잡도로 인해 실행 시간은 증가하였다.

의의
본 논문은 이 작업이 심볼릭 프로토콜 검증 분야의 중요한 진전임을 주장한다. 풀 DH 이론에서의 유니피케이션 불가능성을 극복함으로써, 저자들은 디피-헬먼 그룹의 전체 대수적 구조에 의존하는 더 넓은 범위의 암호 프로토콜을 자동 검증할 수 있게 하였다. ElGamal을 자동으로 검증하고 몇 분 만에 MQV 공격을 재발견할 수 있는 능력은, 이론적 대수 성질과 실용적인 자동 보안 분석 사이의 간극을 메우는 이 접근 방식의 실현 가능성, 확장성 및 효율성을 입증한다.