[Tamarin-prover] Ep 4. Model Specification using Rules

Model Specification using Rules

Tamarin 모델들은 3가지 주요 성분을 가지고 제작한다.

• Rules
• Facts
• Terms

우리는 이미 이전 섹션에서 해당 용어들에 대한 정의를 보았다. 이제 Naxos protocol을 통해 facts와 rules의 사용법을 알아보자.

출처 : https://tamarin-prover.com/manual/master/book/005_protocol-specification-rules.html

해당 프로토콜에서는, 각 참여자 x는 long-term private key인 lkx와 이에 대응하는 public key pkx = 'g'^lkx를 가지고 있다. (g는 Diffie-Hellman 그룹의 generator를 의미한다) g의 값이 공개 값이기 때문에, 우리는 이것을 공개 상수로써 모델링 한다.
여기서는 두 개의 서로 다른 해시 함수 h1과 h2가 사용되었다.

---

위 그림의 프로토콜은 다음과 같이 나타낼 수 있다.

1. initiator I는 새로운 nonce eskI를 생성한다. (eskI는 I's ephemeral (private) key를 의미한다)
2. I의 long-term private key lkI와 eskI를 concatenate한 후, 해시 함수 h1을 이용하여 'g'^h1(eskI, lkI)를 responder R에게 전송한다.
3. R은 전달 받은 값을 변수 X에 저장하고, R이 선택한 nonce인 eskR과 long-term private key lkR을 기반으로 생성한 'g'^h1(eskR, lkR)을 I에게 전송한다.
4. I는 전송받은 값을 변수 Y에 저장한다.

두 참가자는 각자의 long-term private keysession key kI와 kR을 각각 계산할 수 있게 된다.

교환된 메시지들은 수신자들이 메시지 생성에 사용된 long-term key를 검증할 수 없기 때문에 인증되지는 않는다. 인증은 암묵적이고 오직 정당한 키의 소유권을 통해서만 보장된다. 명시적인 인증(e.g. 의도된 상대방이 최근까지 활성 상태였거나 특정 값에 대해 합의했다는 보장)은 key-confirmation 단계(각 참가자들이 계산된 세션 키를 통해 생성된 교환된 메시지의 MAC을 교환하는 과정)를 추가함으로써 인증된 키 교환 프로토콜(AKE protocol, Authenticated Key Exchange protocol)에서 수행된다.

참고
Naxos 프로토콜의 자세한 내용은 다음 자료를 참고해라.
LaMacchia, B., Lauter, K., & Mityagin, A. (2007, November). Stronger security of authenticated key exchange. In International conference on provable security (pp. 1-16). Berlin, Heidelberg: Springer Berlin Heidelberg.

Rules

우리는 프로토콜과 공격자의 동시 실행을 명시하기 위해 멀티셋 재작성(multiset rewriting)을 사용한다. (공격자가 프로토콜을 수행하는 참여자들과 병렬로(=동시에) 상호작용하는 상황을 다루겠다는 의미로써, 공격자는 eavesdropping, modification, forgery, replay 할 수 있는 능력을 가진다)
멀티셋 재작성은 독립적인 전이를 지원하기 때문에 동시 시스템을 모델링하는 데 일반적으로 사용된다.

멀티셋 재작성 시스템은 전이 시스템을 정의하며, 우리의 경우 전이는 라벨이 지정된다.
이 시스템의 상태는 fact의 멀티셋(또는 bag)으로 표현된다.

Tamarin에서 재삭성 규칙은 이름과 세 part를 가진다.
각각, rule의 LHS, 라벨이 지정된 전이(action fact라 부른다), rule의 RHS

rule MyRule1:
	[ ] --[ L('x') ]-> [ F('1', 'x'), F('2', 'y') ]
    
rule MyRule2:
	[ F(u,v) ] --[ M(u,v) ]-> [ H(u), G(`3`, h(v)) ]

rule의 이름은 중복되지 않는 한, 임의로 정할 수 있다.(이름에는 어떠한 의미도 없다)

Executions

전이 시스템의 초기 상태는 빈 멀티셋이다.
규칙들은 시스템이 새로운 상태로 전이를 만들 수 있는지 정의한다. 어떤 규칙이 현재 상태에 적용될 수 있으려면, 해당 규칙의 LHS가 현재 상태를 포함될 수 있도록 인스턴스화(instantiation)할 수 있어야 한다. 이 경우에, LHS 사실(facts)들은 현재 상태에서 사라지고 인스턴스화된 RHS의 fact로 교체된다.

예를 들어서, 초기 상태에서 MyRule1이 반복적으로 인스턴스화 되어질 수 있다.

어떤 방식으로든 MyRule1의 인스턴스화는 후속 상태가 F('1', 'x'), F('2', 'y')를 포함하는 것을 야기한다.
MyRule2 규칙은 초기 상태가 F 사실을 포함하고 있지 않기 때문에 초기 상태에서는 적용될 수 없다.
successor state(MyRule1이 적용된 후의 상태(후속 상태))에서는 MyRule2가 두 번 적용될 수 있다.

• u = '1', v = 'x'로 인스턴스화 될 수 있음.
• u = '2', v = 'y'로 인스턴스화 될 수 있음.
  이러한 각 인스턴스화는 새로운 후속 상태(successor state)로 이어지게 된다.

Using 'let' binding in rules for local macros

더 복잡한 프로토콜을 모델링할 때, 한 용어(term)는 같은 rule에서 여러번 나타날 수 있다. 이러한 명세들의 가독성을 높이기 위해서, Tamarin은 let ... in 키워드를 지원한다.

rule MyRuleName:
	let foo1 = h(bar)
    	foo2 = <'bars', foo1>
        ...
        var5 = pk(~x)
    in
    [ ... ] --[ ... ]-> [ ... ]

이러한 let-binding 표현식은 규칙의 문맥 내에서 로컬 term 매크로를 지정하는 데 사용할 수 있다.
각 매크로는 별도의 줄에서 정의되어야 하며, substitution을 의미한다( LHS는 반드시 변수이어야 하고, RHS는 임의의 항(term)이 될 수 있다)
규칙은 let-binding에서 정의된 변수를 모두 해당 RHS의 값으로 치환된 후 해석된다. 또한, 위의 예제에서 볼 수 있듯이, 매크로는 앞서 정의된 매크로의 좌변 값을 사용할 수도 있다.

Global macros

때때로 우리는 여러 rules에서 동일한 let-binding(s)을 사용하길 원한다. 이 경우에는, macros 키워드를 사용하여 global macros로 선언할 수 있다. 이 전역 매크로는 모든 rules에서 사용가능하다.

macros: macro1(x) = h(x), macro2(x, y) = <x, y>, ... , macro7() = $A

여기서 macro1은 첫 번째 매크로의 이름이며, x는 해당 매크로의 매개변수이다.
= 기호의 오른쪽에 있는 항(term)은 매크로의 출력이며, 해당 매크로가 반환하는 값이다
규칙(rule)에서 매크로를 사용하려면, 해당 매크로를 함수처럼 항 내부에서 호출하면 된다.

[ In(macro1(~ltk)) ] --[ ... ]-> [ Out(macro2(pkA, pkB)) ]

위 예제는 매크로가 적용되고 나면 다음과 같이 바뀌게 될 것이다.

[ In(h(~ltk)) ] --[ ... ]-> [ Out(<pkA, pkB>) ]

후속 매크로가 먼저 정의 되어 있다면, 매크로는 후속 매크로(second macro)를 호출할 수 있다

macros: innerMacro(x, y) = <x, y>, hashMacro(x, y) = h(innerMacro(x, y))

밑의 예시는 에러이다.

macros: hashMacro(x, y) = h(innerMacro(x, y)), innerMacro(x, y) = <x, y>

hashMacro가 정의되었을 때, innerMacro가 아직 정의되어지지 않았기 때문이다.

매크로는 규칙(rule)에만 적용되며, Interactive mode에서 프로토콜 규칙과 함께 표시된다.

Facts

Tamarin에서 Fact는 프로토콜 실행의 상태를 나타내는 요소이다. Fact는 고정된 arity(매개변수 개수)를 가지며, 형식은 다음과 같다.

• F는 Fact의 이름(심볼)이며, t는 해당 fact에 포함된 변수 또는 값이다.

Tamarin에는 내장된 특수한 Fact 3가지가 존재한다.

1) In()

• 신뢰할 수 없는 네트워크에서 메시지를 받는 것을 의미
• 공격자가 제어하는 네트워크에서 메시지를 수신하는 상황을 모델링
• 재작성 규칙의 LHS에서만 사용 가능

2) Out()

• 신뢰할 수 없는 네트워크로 메시지를 보내는 것을 의미
• 공격자가 접근할 수 있는 채널을 통해 메시지가 전송됨
• 재작성 규칙의 RHS에서만 사용 가능

3) Fr()

• 고유한 난수(fresh value)를 생성하는 역할
• 재작성 규칙의 LHS에서만 사용 가능
• Tamarin의 내장 규칙에 의해서 Fr(x)는 항상 다른 새로운 값을 생성

Linear versus persistent facts

위에서 언급한 사실(facts)들은 '선형 사실(linear facts)'라고 불린다. 이들은 규칙에 의해 생성될 뿐만 아니라, 규칙에 의해 소멸될 수도 있다. 따라서, 특정 상태에서는 존재할 수 있지만 다른 상태에서는 사라질 수도 있다.

반면, 일부 사실은 한 번 도입되면 절대로 상태에서 사라지지 않는다. 이러한 사실을 선형 사실을 사용하여 모델링하려면, 해당 사실이 LHS에 포함된 모든 규칙에서 동일한 사실을 RHS에도 복사해야 한다. 이론적으로는 문제가 없지만, 사용자에게 불편할 수 있으며, Tamarin이 해당 사실을 추적하는 데 불필요한 규칙 인스턴스화를 탐색할 수도 있다.

지속적 사실(persistent facts)는 fact이름 앞에 ! 키워드를 붙여 선언한다. 절대 소멸되지 않는 사실을 모델링할 때는 지속적 사실을 사용하는 것이 선호된다.