Cryptology Academy · 강의

Tamarin과 계산적 증명

Tamarin 증명기를 사용해 다중 집합 재작성과 추적 기반 검증을 수행합니다.

Tamarin과 계산적 증명은(는) CoddyKit의 무료 Cryptology Academy 강의입니다. 이것은 4개 중 4번째 강의입니다. 아래에서 전체 강의를 무료로 읽을 수 있으며, 내장 코드 에디터와 24/7 AI 튜터와 함께 브라우저에서 직접 실습할 수 있습니다. 이 강의는 Cryptology Academy 학습 경로의 일부이며, 진행 상황이 웹과 CoddyKit 앱에 동기화됩니다. Cryptology Academy 강의에는 총 4개의 강의가 포함되어 있습니다.

Tamarin이란 무엇입니까

Tamarin(ETH Zurich, 2012)은 다중 집합 다시 쓰기를 기반으로 하는 보안 프로토콜 검증 도구입니다. 혼 절 접근 방식을 사용하는 ProVerif와 달리, Tamarin은 대화형 증명기를 사용해 프로토콜 실행의 실행 추적을 추론합니다.

Tamarin과 ProVerif 비교

ProVerif: 완전 자동화되지만 "cannot be proved"를 출력할 수 있습니다. Tamarin: 대화형 증명 보조 도구와 자동 모드를 함께 제공하며, 등식 이론(XOR, 디피-헬먼, 쌍선형 사상)을 처리합니다. 표현력이 더 뛰어나지만 학습 곡선이 더 가파릅니다.

다중 집합 다시 쓰기 규칙

Tamarin은 사실에 대한 다시 쓰기 규칙으로 프로토콜을 모델링합니다. 사실은 상태를 나타냅니다. [ L ] --[ A ]-> [ R ] 규칙은 왼쪽 사실 L을 소비하고, 오른쪽 사실 R을 생성하며, 동작 A를 실행 추적에 기록합니다.

Tamarin 입력 언어(.spthy)

Tamarin 이론 파일은 함수, 방정식, 규칙 및 보조정리를 선언합니다:

/* Diffie-Hellman key exchange */
builtins: diffie-hellman

rule Alice_1:
  [ Fr(~a) ]  /* fresh random a */
  --[ AliceSent($A, $B, 'g'^~a) ]->
  [ Alice_St($A, $B, ~a), Out('g'^~a) ]

rule Bob_1:
  [ In(ga), Fr(~b) ]
  --[ BobReceived($A, $B, ga) ]->
  [ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]

보조정리 작성

보안 목표는 실행 추적에 대한 보조정리로 표현합니다:

/* Secrecy: shared secret not known to attacker */
lemma secret_key:
  "All A B k #i #j.
    AliceKey(A, B, k) @ i &
    BobKey(A, B, k) @ j
    ==> not (Ex #r. K(k) @ r)"

/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
  "All A B k #j. BobKey(A, B, k) @ j
    ==> Ex #i. AliceKey(A, B, k) @ i & i < j"

Tamarin 실행

Tamarin의 대화형 GUI를 실행합니다: tamarin-prover interactive my_protocol.spthy. 브라우저 UI에는 증명 의무가 표시됩니다. 자동화 전략을 안내하거나 종료되지 않는 경우에 수동 단계를 적용할 수 있습니다.

계산적 건전성

기호적 증명(ProVerif, Tamarin)은 완벽한 암호 가정 아래에서 보안을 보장합니다. 계산적 건전성 정리(Cortier, Backes)는 증명된 보안성을 갖는 기본 요소로 구현할 때 기호적 증명을 계산적 보안으로 확장합니다.

F와 HACL: 검증된 구현

F*(Microsoft Research)는 증명 중심 프로그래밍 언어입니다. HACL*은 F*로 작성된 암호 라이브러리로, 정확성과 부채널 저항성에 대한 기계 검증 증명을 포함합니다. Firefox의 NSS와 mbedTLS에서 사용됩니다.

EasyCrypt: 게임 기반 계산적 증명

EasyCrypt는 프로토콜뿐 아니라 암호 구성에 대해서도 완전한 계산적(게임 기반) 보안 증명을 수행할 수 있게 합니다. TLS 1.3 레코드 계층과 ChaCha20-Poly1305는 EasyCrypt로 검증되었습니다.

실제 적용 효과

형식적으로 검증된 암호 기술이 실제 제품에 도입되고 있습니다. NSS(Firefox)는 HACL*을 사용하고, AWS는 증명 가능한 어설션이 포함된 s2n-tls를 사용하며, Signal 프로토콜은 ProVerif와 Tamarin으로 검증되었습니다. 형식 방법은 더 이상 학계에만 머물지 않습니다.

이해도 확인

자동화가 실패하는 경우 Tamarin은 ProVerif와 달리 어떻게 처리합니까?

단원 요약

Tamarin은 다중 집합 다시 쓰기와 대화형 증명 GUI를 사용하는 실행 추적 기반 추론을 제공합니다. DH와 XOR 등식 이론을 처리합니다. 보조정리는 기밀성과 인증 목표를 표현합니다. 계산적 건전성은 기호적 증명을 실제 보안으로 연결합니다. HACL*과 EasyCrypt는 검증 범위를 구현과 암호 구성으로 확장합니다.

자주 묻는 질문