[Tamarin-prover] Ep 3. Cryptographic Messages

Cryptographic Messages

Tamarin은 암호학(Cryptography)의 기호적 모델(symbolic model)을 사용하여 프로토콜을 분석한다. 즉, 암호화된 메시지를 비트 문자열(bit string)로 다루는 것이 아니라, 수학적 항(term)으로 모델링한다. 사용된 암호 알고리즘의 속성은 방정식(equation)으로 모델링된다. 더 구체적으로, 암호 메시지는 다음 중 하나이다.

• 상수 C
• f(m1, ..., mn) 형태의 메시지: 이는 n개의 암호 메시지 m1, ..., mn에 n항 함수 기호 f를 적용한 결과를 나타낸다.

방정식을 지정할 때, 상수뿐만 아니라 변수도 사용할 수 있다.

Constants

우리는 다음과 같은 유형의 상수를 구별한다.

• 공개 상수(Public constants) : 공개적으로 알려진 원자적 메시지를 모델링하며, 예를 들어 에이전트 식별자 및 레이블이 이에 해당한다. Tamarin에서는 ident 표기법을 사용하여 공개 상수를 나타낸다. 이러한 상수는 pub 유형이며, 공개 변수와 통합(unification)될 수 있다. 항상 공격자가 알고 있는 값이다.

• 아리티(arity)가 0인 함수 (Functions of arity 0) : 항상 msg 유형이며, 공개 변수와 통합될 수 없다. 기본적으로 이 함수는 공개이며, 공격자가 알 수 있는 값이다. 그러나 함수가 private로 선언되면 공격자가 알 수 없는 값이 된다. 하지만 이 비밀 값을 모델링할 때는 보통 fresh값을 사용하는 것이 더 적절하다.

• 자연수(Natural Numbers) : 유일한 상수는 %1 또는 1:nat으로 표현되며, 숫자 1을 모델링한다.

Function Symbols

Tamarin은 내장된 함수 기호(built-in function symbols)와 사용자가 정의할 수 있는 추가 함수 기호(user-defined function symbols)를 지원한다. 모든 Tamarin 파일에서 기본적으로 사용할 수 있는 함수 기호는 쌍(pairing)과 투영(projection)이다.

• 이항(binary) 함수 pair: 두 개의 메시지를 하나의 쌍으로 결합
• fst 와 snd함수 : pair(x, y)에서 각각 첫 번째 요소 x와 y를 추출

이러한 투영 연산은 다음과 같은 방정식으로 정의된다.

fst(pair(x, y)) = x
snd(pair(x, y)) = y

또한 Tamarin은 다음과 같은 구문적 축약(Syntactic sugar)을 지원한다.

<x, y> = pair(x, y)
<x1, x2, ..., ,xn-1, xn> = <x1, <x2, ..., <xn-1, xn> ...>

특정한 메시지 이론(Message theories)를 활성화하면 추가적인 내장 함수 기호를 사용할 수 있다.
hashing, asymmetric-encryption, signing, revealing-signing, symmetric-encryption, diffie-hellman, bilinear-pairing, xor, and multiset.
해당 메시지 이론의 정의는 Built-in message theories섹션에서 확인한다.

Tamarin은 또한 사용자 정의 함수 기호(User-defined function symbol)를 정의할 수 있다. 함수 기호를 정의하려면, 아리티(arity)값을 포함한 다음 줄을 파일에 추가해야 한다.

functions: f1/a1, ..., fn/an

여기서 f1/a1은 함수 f1이 a1개의 인수를 가진다는 의미

마지막으로, 비공개 함수 기호(Private function symbol)를 지원한다. 일반적인 함수 기호와 달리, 비공개 함수는 공격자가 사용할 수 없는 함수로 가정한다. 비공개 함수는 정직한(honest) 사용자들 사이에서 공유되는 비밀(secret)을 암시적으로 포함하는 함수를 모델링할 때 사용될 수 있다. 함수를 비공개로 만들려면, 함수 뒤에 [private] 속성을 추가하면 된다.

functions: f/3, g/2 [private], h/1

여기서 g는 비공개 함수이고, f, h는 공개 함수이다.

Equational theories

방정식 이론은 함수의 속성을 모델링하는 데 사용될 수 있다.
예를 들어, 대칭키 복호화가 대칭키 암호화의 역연산(inverse)이라는 성질을 표현할 수 있다.
방정식을 Tamarin의 컨텍스트(context)에 추가하려면 다음과 같은 구문을 사용한다.

equations: lhs1 = rhs1, ..., lhsn = rhsn

좌변(lhs)과 우변(rhs) 모두 변수를 포함할 수 있지만, 공개 상수(public constants)는 포함할 수 없다. 또한, 우변에 있는 모든 변수는 반드시 좌변에도 등장해야 한다.
Tamarin에서 사용되는 기호적 증명 탐색(symbolic proof search)은 특정한 사용자 정의 방정식 클래스, 즉 유한 변형 속성(finite variant property)을 가지는 수렴 방정식 이론(convergent equational theories)을 지원한다.
Tamarin은 주어진 방정식이 이 클래스에 속하는지 검사하지 않으므로, 해당 클래스를 벗어나는 방정식을 작성하면 무한 루프 또는 잘못된 결과가 발생할 수 있으며, 이에 대한 경고과 표시되지 않는다. 또한, Tamarin의 추론은 부분항 수렴 방정식만 고려할 때 특히 효율적이다. 즉, 우변이 기저 항(ground term, 변수를 포함하지 않는 항)이거나 좌변이 진부분항(proper subterm)인 경우, Tamarin의 효율성이 향상된다.
따라서, 필요한 속성을 모델링하는 데 충분한 경우 이러한 형태의 방정식이 선호된다.

그러나, Diffie-Hellman, bilinear-pairing, XOR, multiset과 같은 내장 메시지 이론에서 모델링된 방정식은 이러한 제한된 클래스에 속하지 않는다.
이는 예를 들어, 결합법칙(associativity)과 교환법칙(commutativity)을 포함하기 때문이다. 기타 모든 내장 메시지 이론은 functions: ... 및 equations: ...을 사용하여 동일하게 정의할 수 있으며, 다음 섹션에서 허용되는 방정식의 예시를 살펴보자.

Built-in message theories and other built-in features

f/n은 함수 기호 f가 n개의 인수를 가진 함수(arity n)임을 나타낸다.

hashing: 해시 함수를 모델링한다. 함수 기호는 h/1이고, 방정식은 없다.

asymmetric-encryption

• 정의: 공개키 암호화(public key encryption scheme) 모델
• 함수 기호: aenc/2, adec/2, and pk/1
• 방정식: adec(aenc(m, pk(sk)), sk) = m
• 구문적 축약: aenc{x, y}pkB = aenc(<x, y>, pkB)

signing

• 정의: 전자 서명(signature) 모델
• 함수 기호: sign/2, verify/3, pk/1, and true
• 방정식: verify(sign(m, sk), m, pk(sk)) = true

revealing-signing

• 정의: 메시지가 공개되는 서명 모델
• 함수 기호: revealSign/2, revealVerify/3, getMessage/1, pk/1, and true
• 방정식:

revealVerify(revealSign(m, sk), m, pk(sk)) = true
getMessage(revealSign(m, ks)) = m

symmetric-encryption

• 정의: 대칭키 암호화(symmetric encryption scheme) 모델
• 함수 기호: senc/2 and sdec/2
• 방정식: sdec(senc(m, k), k) = m

diffie-hellman

• 정의: 디피-헬만 그룹 모델
• 함수 기호: inv/1, 1/0, ^, and *
• 방정식:

(x^y)^z = x^(y*z)
x^1 = x
x*y = y*x
(x*y)*z = x*(y*z)
x*1 = x
x*inv(x) = 1

bilinear-pairing

• 정의: 쌍선형 그룹 모델
• 함수 기호: pmult/2, em/2
• 방정식:

pmult(x, pmult(y, p)) = pmult(x*y, p)
pmult(1, p) = p
em(p, q) = em(q, p)
em(pmult(x, p), q) = pmult(x, em(q, p))

xor

• 정의: 배타적 논리합(XOR) 연산 모델
• 함수 기호: ⊕/2(또는 XOR/2), zero/0
• 방정식:

x ⊕ y       = y ⊕ x
(x ⊕ y) ⊕ z = x ⊕ (y ⊕ z)
x ⊕ zero    = x
x ⊕ x       = zero

multiset

• 정의: 다중집합 연산을 위한 모델
• 함수 기호: ++
• 속성: 결합법칙 및 교환법칙 적용

natural-numbers

• 정의: 카운터(counter) 모델링
• 함수 기호: %+(덧셈 연산자), and %1
• 속성:
  • 모든 자연수 값은 공개(public knowledge)이며, 공격자가 직접 구성할 필요 없음
  • 주로 작은 숫자(카운터 등)를 모델링하는 데 사용
  • 큰 랜덤 숫자를 모델링할 때는 fresh 변수를 사용하는 것이 권장됨
• WPA-2 프로토콜 예시

<~x, %n>

• ~x : 랜덤한 시작값
• %n : 공격자가 추측할 수 있는 카운터 값

reliable-channel

• 정의: 프로세스 계산에서 신뢰할 수 있는 채널을 지원
• 채널 종류:
  • r : 신뢰할 수 있는 채널 (메시지는 반드시 도착)
  • c : 공개 및 신뢰할 수 없는 채널
• 다중 채널 모델링 예시

out('r', <'channelA', 'Hello')
| out('r', <'channelB', 'Bonjour')
| in('r', <'channelA', x); event PrepareTea()
| in('r', <'channelB', x); event PrepareCoffee()

Reserved function symbol names

다음 함수 이름들은 사용자 정의 함수의 이름으로 사용될 수 없다.
mun, one, exp, mult, inv, pmult, and em.
어떤 이론에서 위 함수 기호 중 하나라도 사용자 정의 함수로 표현하면, parser는 해당 파일을 거부하며, 어떤 예약된 이름이 재정의되었는지를 명확히 표시할 것이다.