기술 요약: Tamarin에서 ProVerif로의 건전한 번역 (A Sound Translation from Tamarin to ProVerif)

문제 정의

프로토콜 검증 도구인 Tamarin과 ProVerif는 보안 프로토콜의 형식적 분석에서 매우 중요하지만, 서로 근본적으로 다른 형식 체계를 사용하므로 체계적인 비교와 상호 보완적인 강점 활용을 방해한다.

• Tamarin은 제약 해결(constraint solving)을 동반한 **다중 집합 재작성 규칙(Multiset Rewrite Rules, MSRs)**을 사용한다. 이는 건전하고 완전한(sound and complete) 검증을 제공하여 허위 공격(spurious attacks)을 제거하지만, 효율성 문제와 비종료(non-termination) 문제를 겪을 수 있다.
• ProVerif는 applied-$\pi$ calculus와 Horn 절 추상화를 채택한다. 일반적으로 더 빠르고 백트래킹을 피할 수 있지만, 과잉 근사(over-approximation)로 인해 허위 공격(spurious attacks, 불완전한 결과)을 생성할 수 있다.

두 도구 간의 번역 메커니즘이 부족하여, 어떤 속성이 양쪽 모두에서 검증 가능한지 결정하거나, 의미론적으로 동일한 모델에 대해 성능을 비교하거나, Tamarin 모델의 빠른 백엔드로 ProVerif를 사용하는 것이 어렵다. 기존 연구는 applied-$\pi$에서 MSRs로의 번역(예: SAPiC+에서 Tamarin으로)이나 제한된 범위의 이론적 연결에 집중했으나, Tamarin에서 ProVerif로의 포괄적이고 건전한 번환은 누락되어 있었다.

방법론

저자들은 MSRs와 applied-$\pi$ calculus 사이의 간극을 메우는 **건전한 번역(sound translation)**을 제시한다. 이 번역은 세 가지 주요 구성 요소로 이루어진다.

1. 규칙 번역 (프로세스 생성)

Tamarin 규칙은 병렬 ProVerif 프로세스로 번역된다.

• 상태 관리: Tamarin의 사실(fact) 다중 집합은 ProVerif의 **테이블(tables)**을 사용하여 에뮬레이션된다. ProVerif의 테이블은 단조 증가(monotonic)하므로(항목을 삭제할 수 없음), 이는 초기에 Tamarin의 선형적 사실 소비를 과잉 근사하게 된다.
• 다중 집합 의미론: 선형 사실의 "단 한 번 소비(consume once)" 의미론을 보존하기 위해, 번역은 **새로운 규칙 인스턴스 식별자(fresh rule-instance identifiers)**를 도입한다. 모든 선형 저장 사실에 대해 고유한 식별자가 생성되어 저장된다. 동일한 식별자와 인수를 가진 두 개의 이벤트가 발생하지 않도록 하는 제한(restriction)이 추가되어, 효과적으로 선형 소비를 강제한다.
• 패턴 매칭: Tamarin은 사실에 대한 패턴 매칭(예: 암호화된 항에서 변수 추출)을 허용한다. ProVerif의 입력은 튜플 패턴만을 지원한다. 번역은 복잡한 패턴에서 변수를 추출하기 위해 **사적인 보조 파괴자(private auxiliary destructors)**를 도입하며, 이러한 기능이 공격자에게 노출되지 않도록 보장한다.
• 통신: 네트워크 입력(In) 및 출력(Out)은 전역 공용 채널상의 ProVerif in 및 out으로 매핑된다. 새로운 이름(Fr)은 new로 매핑된다.

2. 레마 번역 (속성 재작성)

Tamarin 레마는 ProVerif 쿼리로 번역된다. 번역은 Tamarin의 2-정렬 1차 논리와 ProVerif의 SA-QBF(Single-Alternation Quantified Boolean Formulas) 파편 간의 논리적 차이를 처리한다.

• 한정사 처리: Tamarin의 명시적 한정사는 ProVerif의 암묵적 한정사(보편 한정된 전제 변수, 존재 한정된 결론 변수)로 매핑된다.
• 논리적 재작성:
  • 논리합/논리곱: exists-trace 레마의 최상위 논리합(disjunctions)과 all-trace 레마의 논리곱(conjunctions)은 여러 ProVerif 쿼리로 분할된다. 결과는 논리적으로 재결합된다(예: 존재성을 위해 분할된 쿼리 중 하나라도 성립하면 레마가 성립하거나, 보편성을 위해 모두 성립해야 함).
  • 부정: ProVerif는 쿼리 내에서 부정을 지원하지 않는다. 번역은 논리적 동등성을 사용하여 부정을 이동시키며, 종종 모든 all-trace 속성을 역전된 결과를 가진 도달 가능성(reachability) 쿼리로 변환한다.
• 동시 이벤트: Tamarin은 동일한 시점에 여러 액션 사실을 허용한다. 번역은 동일한 규칙에서 나온 이벤트들에 공유된 규칙 인스턴스 식별자를 할당하여, 전순서(total order)를 가정하는 ProVerif가 동시성을 시뮬레이션할 수 있도록 한다.
• 지식 사실: Tamarin의 K(m)(공격자가 m을 명시적으로 유도함)은 특정 극성 제약 조건(all-trace 속성의 가설 내 양의 원자) 하에서 ProVerif의 attacker(m)로 번역된다.

3. 의미론적 간극 브릿징

• 동시성: 이벤트들을 묶기 위한 규칙 인스턴스 식별자를 통해 처리된다.
• 함의 의미론: 번역은 필요에 따라 진행 제한(progress restrictions)을 사용하여, 시간적 순서에 관한 Tamarin과 ProVerif의 미묘한 함의(=>) 해석 차이를 고려한다.
• 지원되지 않는 기능: Tamarin의 다중 집합 빌트인, 쌍선형 페어링(bilinear pairings), 역원이 있는 디피-헬먼(Diffie-Hellman with inverse) 등의 기능은 제외된다. XOR은 ProVerif의 결합 법칙 기호 부재로 인해 건전성 보장 범위 밖의 "최선 노력(best-effort)" 근사치로 번역된다.

주요 기여

1. 건전한 번역: ProVerif에서 검증된 모든 속성이 (충실한 파편 내에서) 원래의 Tamarin 모델에서도 성립함을 보장하는 Tamarin에서 ProVerif로의 형식적 번역.
2. 새로운 인코딩 기법: (식별자와 제한을 사용하여) 다중 집합 재작성 의미론을 인코딩하고, 전순서를 가정하는 계산법에서 동시 이벤트를 처리하는 기술.
3. 논리 파편 특성화: 두 도구가 공유하는 공통 핵심 논리 파편(TSA-QBF)을 식별하여, 어떤 속성이 충실하게 번역될 수 있는지 정확히 정의함.
4. 대규모 실증 연구: 566개의 레마 태스크를 포함하는 121개의 Tamarin 모델에 대한 평가를 통해, 이 두 도구를 의미론적으로 동일한 모델에 대해 수행한 최초의 대규모 비교 분석을 제공함.

결과

평가는 121개 모델(566개 레마 태스크)을 대상으로 수행되었다.

• 번역 커버리지: 번역은 566개 중 562개(99.3%)의 태스크에 대해 쿼리 생성을 성공적으로 완료했다.
• 일치성: 확정적인 결과를 가진 비-XOR 태스크 쌍 중에서, 247개 중 246개가 일치했다. 단 하나의 불일치는 불완전한 모델 번역으로 분류되었다.
• 성능:
  • 속도: ProVerif는 비교 가능한 362개 케이스 중 334개(92.3%)에서 더 빨랐다. 중앙값 실행 시간 비율은 ProVerif가 6.74배 더 빨랐다.
  • 메모리: ProVerif는 현저히 적은 메모리를 사용했으며, 중앙값 피크 메모리 비율은 Tamarin보다 6.24배 낮았다.
  • 사례 연구: Andrew Secure RPC 프로토콜의 Lowe 수정 버전에서, ProVerif는 5개의 일치하는 레마에 대해 64.7배 더 빨랐으며, 가장 복잡한 주입적 합의(injective agreement) 레마의 경우 129.6배 더 빨랐다.
• 건전성 보장: 번역은 충실한 파편(faithful fragment)에 대해 건전하다. exists-trace 속성이 공격자 지식 사실을 포함하지 않는 경우, 번역은 또한 완전하다(Tamarin이 트레이스를 찾는다면 ProVerif도 이를 찾을 것이다).

의의 및 주장

본 논문은 Tamarin과 ProVerif 간의 비교 분석을 위한 엄격한 토대를 제공한다고 주장한다. Tamarin 모델을 ProVerif로 번역함으로써 저자들은 다음을 입증한다.

• 두 도구 사이에 상당한 공통 핵심 논리 파편이 존재한다.
• (모델이 충실한 번역 파편 내에 머무는 한) ProVerif의 성능 우위(속도 및 메모리 효율성)를 건전성을 희생하지 않고 활용할 수 있다.
• 번역은 Tamarin의 빠른 백엔드 역할을 수행하여, 사용자가 비-주입적(non-injective) 및 주입적 합의(injective agreement) 속성을 신속하게 검증할 수 있게 한다.
• 본 연구는 의미론적 간극(예: XOR 처리, 다중 집합 의미론, 부정 처리)을 강조하며, 어떤 부분이 번역 가능하고 어떤 부분이 최선 노력 기반의 근사치인지, 혹은 불가능한지를 정확히 규명한다.

저자들은 이 번역이 모든 Tamarin 기능(특히 다중 집합 빌트인 및 특정 DH 모델 제외)에 대해 완전하지는 않지만, 실질적인 보안 속성의 광범한 부분집합을 다루고 있어 체계적인 실증 연구를 가능하게 한다고 강조한다. 결과는 많은 표준 프로토콜에 대해, 정의된 파편 경계 내에서 사용될 때 ProVerif가 Tamarin의 매우 효율적인 대안 또는 보완재가 될 수 있음을 시사한다.