기술 요약: FO 기반 KEM을 위한 검증 가능한 복호화 테스트

문제 정의

Fujisaki–Okamoto(FO) 변환에 기반한 양자 내성 키 캡슐화 메커니즘(KEM)은 결정적인 복호화 검사 과정에 의존한다: 즉, 알고리즘은 암호문을 복호화하고, 암호화 무작위성을 재도출하며, 암호문을 재계산한 뒤, 공유 비밀을 도출하기 전에 이를 수신된 것과 비교해야 한다. 이러한 검사는 보안상 매우 중요하지만, 표준적인 블랙박스 입출력 테스트는 특정 구현 결함을 감지하지 못할 수 있다. 어떤 구현체는 재암호화 계산의 일부를 누락하거나 분기 선택 로직을 변경하면서도, 정직하게 생성된 암호문에 대해서는 기대하는 공유 비밀을 그대로 반환함으로써, 보안 검사를 우회하면서도 표준 테스트 하네스에서 오류를 발생시키지 않을 수 있다.

본 논문은 KEM이 확인 코드(confirmation codes)로 보강되었을 때, 블랙박스 테스트를 통해 FO 기반 복호화 검사의 실행에 대해 무엇을 공식적으로 인증할 수 있는지에 대한 질문을 다룬다.

방법론 및 모델

저자들은 정직한 참조 하네스(honest-reference harness) 하에서 테스트되는 확인 코드 보강형 FO 복호화에 관한 공식 이론을 제안한다.

보강된 구조

이 모델은 최종 키 도출 과정에 숨겨진 확인 위트니스(confirmation witness) $W$를 도입하여 표준 FO 기반 KEM을 확장한다.

1. 캡슐화(Encapsulation): 암호문과 내부 확인 값 $W$를 생성한다. 최종 키 $K$는 $K = G_K(\langle \text{good}, B, W \rangle)$로 도출된다. 여기서 $B$는 국소적 트랜스크립트 접두사이며 $G_K$는 랜덤 오라클이다.
2. 복호화(Decapsulation): 암호문과 확인 위트니스 $W'$를 재계산한다. 최종 키는 $W' = W$인 경우에만 도출된다.
3. 정직한 참조 하네스(Honest-Reference Harness): 테스트 하네스는 복호화 입력(암호문, 키)을 제공하지만, 숨겨진 위트니스 $W$와 최종 키 $K$는 제공하지 않는다. 테스트 대상 시스템(SUT)은 올바른 튜플 $\langle \text{good}, B, W \rangle$를 랜덤 오라클 $G_K$에 쿼리하여 올바른 키를 생성해야 한다.

이론적 프레임워크

본 논문은 SUT가 랜덤 오라클에 쿼리하는 후보 위트너스들의 집합을 나타내는 국소적 최종 키 쿼리 리스트 $Q_G(B)$를 정의한다. 이 방법론의 핵심은 "리스트 히트(list-hit)"—즉, 숨겨진 위트니스 $W$가 $Q_G(B)$에 포함되는 사건—의 확률을 분석하여, 결함이 있는 SUT가 테스트를 통과할 확률을 제한하는 것이다.

분석은 다음을 구분한다:

• 정직한 참조 테스트(Honest-Reference Testing): SUT를 건전한 참조로 생성된 피어(peer)와 비교한다.
• 정직한 자기 자신 테스트(Honest-Self Testing): SUT를 자기 자신(캡슐화와 복호화 모두 SUT로부터 수행)과 비교한다.
• 의존성 콘(Dependency Cones): 관측 가능한 타겟 벡터(트랜스크립트 및 최종 키)에 실제로 영향을 미치는 연산들의 집합을 식별한다.

주요 기여

1. 타이트한 리스트-히트 탐지 가능성 정리 (Tight List-Hit Detectability Theorem)

중심 결과(정리 5.1)는 $q$-국소적 SUT에 대해, 정직한 참조 하네스 하에서의 통과 확률이 다음과 같이 제한됨을 확립한다:
$$\text{Pass} \leq \delta_{\Pi_C} + \epsilon_{\text{alias}} + \epsilon_{\text{fresh}} + \Pr[W \in Q_G(B)] + 2^{-\kappa}$$
여기서:

• $\delta_{\Pi_C}$는 정직한 정확성 오류이다.
• $\epsilon_{\text{alias}}$는 적대적 에일리어싱(최종 키 인코딩에서의 충돌)을 설명한다.
• $\epsilon_{\text{fresh}}$는 최종 키 신선도 결함(숨겨진 지점의 누출)을 설명한다.
• $\Pr[W \in Q_G(B)]$는 리스트-히트 항으로, SUT가 숨겨진 위트니스를 추측할 확률을 나타낸다.
• $2^{-\kappa}$는 랜덤 오라클 일치 항이다.

본 논문은 이 경계가 타이트함을 증명한다(정리 5.2). 즉, $W$를 예측하는 어떤 예측 모델이라도 SUT의 뷰(view)로부터 $W$를 예측하는 것은 SUT의 통과 확률이 해당 예측자의 성공률과 일치하는 1-쿼리 SUT를 유도한다. 따라서 리스트-히트 항은 하네스가 측정하는 근본적인 장애물이다.

2. 리스트-히트 항을 제한하는 두 가지 경로

본 논문은 피할 수 없는 리스트-히트 항을 제한하는 두 가지 구별된 방법을 제공한다:

• 소스 보안 경로 (cUP-faithful): 하네스가 "cUP-충실(cUP-faithful)"하다면(소스 확인 코드 예측 불가능성 게임에 충실하다면), 리스트-히트 확률은 $q \cdot \epsilon_{\text{cUP}}$로 제한된다. 여기서 $\epsilon_{\text{cUP}}$는 소스 게임에서의 단일 후보 적대자의 이득(advantage)이다. 이는 소스 보안 증명을 선형적인 쿼리 손실과 함께 테스트 문맥으로 전이시킨다.
• 엔트로피 경로 (Entropic Route): 위트니스 $W$가 SUT의 뷰를 기준으로 평균 조건부 미니 엔트로피 $\lambda$를 가진다면, 리스트-히트 확률은 $q \cdot 2^{-\lambda}$로 제한된다. 이 경로는 소스 cUP 경계가 직접 적용되지 않을 수 있는 진단 코드(예: 절단된 해시)를 수용한다.

3. 의존성-콘 하한 (부정적 결과)

본 논문은 블랙박스 인증의 근본적인 한계를 증명한다(정리 5.37). 만약 어떤 연산이 **서포트-액티브 의존성 콘(support-active dependency cone)**의 외부(즉, 해당 연산을 변경해도 정직한 지원 하에서 관측 가능한 트랜스크립트나 최종 키가 변하지 않는 영역)에 있다면, 어떤 블랙박스 정직한 참조 테스트도 그에 대응하는 "삭제(erasure)"(해당 연산을 건너뛰는 버전의 코드)를 포함하는 구현 클래스에 대해 그 실행을 인증할 수 없다.

• 이러한 연산들에 대해, 인증자의 건전성($\alpha$)과 완전성($\beta$) 오류는 항상 $\alpha + \beta \geq 1$을 만족한다.
• 이는 추가적인 계측(instrumentation), 악의적인 입력, 또는 더 큰 타겟 세트 없이는 블랙박스 테스트가 해당 연산의 실행과 삭제된 실행을 구별할 수 없음을 의미한다.

4. 구현 사례 및 산출물

이 이론는 두 계열에 구현되었다:

• ML-KEM (FIPS 203): 소스 확인 코드 라인(선택된 비압축 계수를 사용)과 진단 아티팩트 변형(ML-KEM-CD1, 1바이트 해시 코드를 사용)을 분석한다.
• HQC (2025년 8월 명세): 확인 코드가 암호문의 절단된 꼬리 부분에서 유도되는 솔티드(salted) FO 변형을 분석한다. 본 논문은 이러한 꼬리 유도 코드에 대해 리스트-히트 항을 제한하는 데 필요한 가정인 HQC-TailEnt를 정의한다.

저자들은 다음을 포함하는 재현 가능한 산출물 FO-FaultBench를 제공한다:

• 고정된 베이스라인 (mlkem-native, H%，HQC August 2025).
• 변형된 변이체 (VSFO/CD1, CD*).
• 변이 카탈로그 (바인딩 결함, 결정 결함, 대칭 결함).
• 실험 실행 기록이 담긴 동결된 JSONL 레코드.

실험 결과

산출물 캠페인은 이론적 주장을 검증한다:

• 바인딩 결함 (Binding Faults): 확인 코드를 누락하거나 덮어쓰는 결함은 정직한 참조 테스트 하에서 탐지된다. 이는 최종 키의 입력을 변경하기 때문이다.
• 결정 전용 결함 (Decision-Only Faults): 분기 선택에만 영향을 주는 결함(예: 항상 'good' 키를 선택)은 정직한 암호문에 대해서는 탐지되지 않으나, 악의적이거나 차등적인(differential) 하네스 하에서는 탐지된다. 이는 서포트-일치(support-coincidence)의 한계를 확인시켜 준다.
• 대칭 결함 (Symmetric Faults): 캡슐화와 복호화 모두에 적용된 결함은 셀프 테스트는 통과하지만 정직한 참조 테스트는 실패하며, 이는 피어 모델의 필요성을 입증한다.
• 확률적 추측 (Probabilistic Guessing): 확인 코드를 추측하는 변이체는 유지된 코드 길이에 따른 $2^{-L}$의 확률로 통과하며, 이는 이론적 엔트로피 경계와 일치한다.
• 범위 예산 (Range Budgets): HQC 변형(CD1 vs. CD*)에 대한 실험은 유지된 꼬리 비트(5비트에서 37비트로)를 늘리는 것이 추측 변이체의 통과 확률을 크게 낮춤을 보여주며, 엔트로피 경로를 검증한다.

의의 및 주장

본 논문은 FO 기반 KEM에 대해 블랙박스 테스트가 무엇을 인증할 수 있고 무엇을 할 수 없는지를 정확하게 구분하는 확인 코드 테스트의 공식 이론을 제공한다고 주장한다.

• 긍정적 주장: 본 논문은 확인 코드 바인딩이 재암호화 결함에 대한 탐지 가능한 신호를 생성함을 입증한다(소스 cUP이나 조건부 엔트로피에 의해 리스트-히트 항이 제한되는 경우). 또한 실험 결과를 해석하기 위한 엄격한 프레임워크를 제공한다.
• 부정적 주장: 본 논문은 블랙박스 정직한 참조 테스트에 내재된 한계를 명시적으로 밝힌다. 하네스 타겟을 변경하거나 계측을 추가하지 않는 한, 의존성 콘 외부의 연산(예: 일부 계수만 바인딩된 경우의 전체 재암호화 실행)은 인증할 수 없다.
• 겸손함: 저자들은 본 논문의 정리들이 고전적인 랜덤 오라클 모델(ROM)에 관한 것임을 강조한다. 이들은 기초적인 KEM의 IND-CCA 보안을 재증명하는 것이 아니라, 구성 수준의 보안을 위해 인용된 소스 분석에 의존한다. "보안"은 보강된 라인으로부터 상속되는 것이며, 본 논문의 기여는 테스트 신호와 특정 하네스 설정 하에서의 통과 확률 해석이다.

이 연구는 이론적 보안 게임(cUP, fCOR)과 실제 구현 테스트 사이의 가교 역할을 하며, 포스트 퀀텀 KEM 구현에 대한 실험 결과를 해석하기 위한 "주장 문법(claim grammar)"을 제공한다.