[Tamarin-prover] Ep 1. Introduction

Reference

Tamarin Homepage

Introduction

Tamarin prover(이하 Tamarin)는 보안 프로토콜의 심볼릭 모델링과 분석을 위한 툴이다.
보안 프로토콜 모델을 입력으로 받아, 프로토콜을 실행하는 에이전트들이 다양한 역할(예: 프로토콜 시작자(Initiator), 응답자(Responder), 신뢰할 수 있는 키 서버)에서 취하는 행동을 명시하고, 적대자의 명세와 프로토콜의 원하는 속성을 명시합니다.

Tamarin은 프로토콜의 여러 역할 인스턴스가 병렬로 무작위로 얽혀 실행되더라도, 그리고 공격자의 행동이 함께 포함되더라도, 프로토콜이 지정된 속성을 충족한다는 것을 자동으로 증명할 수 있도록 사용될 수 있다.

Initial Example

https://github.com/tamarin-prover/manual 의 FirstExample.spthy를 이용한다.

Alice-and-Bob notation:

C -> S: aenc(k, pkS)
C <- S: h(k)

client C가 새로운 대칭키 k를 생성하고, server S의 공개키 pkS로 k를 암호화하여 S에게 전달한다.
(aenc는 asymmetric encryption의 약어이다)
서버는 클라이언트에게 k의 해시를 전송함으로써 키의 수신을 확인한다.
적대자 adversary는 Dolev-Yao 모델이기에, 네트워크를 통제하고 네트워크 상의 메시지들을 삭제하고, 삽입하고(Inject), 수정하고 가로챌 수 있다.

Tamarin 파일은 theory 키워드로 시작한다.

theory FirstExample
begin

body는 begin 과 end 키워드 사이에 작성한다.

Cryptographic primitives

builtins는 Tamarin에서 제공하는 함수 API라고 생각하면 된다.
해당 예제에서는 hashing, asymmetric-encryption을 사용한다.
해당 built-ins는 다음과 같은 함수를 제공한다.

• a unary function h, denoting a cryptographic hash function

• a binary function aenc denoting the asymmetric encryption algorithm

• a binary function adec denoting the asymmetric decryption algorithm

• a unary function pk denoting the public key corresponding to a private key

(cf. adec(aenc(m, pk(sk)), sk)는 m을 반환한다.)

Modeling a Public Key Infrastructure

Tamarin에서, 프로토콜과 그 환경을 multiset rewriting rules를 사용하여 모델링 한다.
Rule들은 시스템의 상태에 작용하며, 이 상태는 Fact들의 멀티셋(즉, 중복을 허용하는 집합, bag)으로 표현된다.
여기서 Fact들은 시스템의 상태 정보를 저장하는 논리적 술어(predicates)로써 보여질 수 있다. 즉, 각 사실은 현재 시스템이 어떤 상태에 있는지를 나타내는 역할을 한다.
예를 들어서,
Out(h(k))는 프로토콜이 메시지 h(k)를 퍼블릭 채널에서 보냈다는 것을 의미한다.
In(x)는 프로토콜이 퍼블릭 채널에서 메시지 x를 받았다는 것을 의미한다.

우리는 논쟁에 의해서 주어진 상태에 대한 정보를 저장하기 위해서 fact를 사용한다.
규칙들(rules)은 -->심볼로 분리되는 premise와 conclustion을 가진다.
rule을 실행하는 것은 premise의 모든 fact들이 현재 상태에 존재하는 것을 필요로하고, 실행의 결과로써, premise들이 지워지는 반면에 conclusion에 있는 fact들은 상태에 더해질 것이다.

rule Register_pk:
	[ Fr(~ltk) }
    -->
    [ ~Ltk($A, ~ltk), !Pk($A, pk(~ltk)) ]

이 예제에서 premise는 오직 Fr fact의 인스턴스이다. Fr은 freshly generated name을 의미하는 built-in fact이다. 이러한 매커니즘은 nonces나 keys와 같은 랜덤한 숫자를 모델링하는데 사용된다.

• ~x denotes x:fresh

• $x denotes x:pub

• %x denotes x:national number

• #i denotes i:temporal

• m denotes m:msg

문자열 상수 c는 퍼블릭 네임 pub를 의미한다. 이것은 pub에 속하는 고정된 글로벌 상수이다. (변하지 않는 공용 식별자 같은 역할을 한다.)

---

정렬(Sort)
msg는 최상위 정렬이다. msg 아래에 세 개의 서로 비교할 수 없는(incomparable) 하위 정렬이 존재한다.

• fresh

• pub

• nat
  비교할 수 없다라는 것은 fresh, pub, nat이 서로 포함 관계가 없고, 직접적으로 크기를 비교할 수 없는 독립적인 정렬이라는 뜻이다.

---

시간 변수(Timepoint variables)
시간 변수는 temporal이라는 정렬을 가지며, 서로 연결되지 않은(unconnected) 독립적인 변수들이다.

따라서 위 예제는 다음과 같이 읽힐 수 있다.
먼저 ~ltk (sort of fresh), 새로운 private key를 생성했고, 키 쌍을 생성하기 위한 agent를 위해서 정해져있지 않은(non-deterministically) 공개 이름 A를 선택했다. 그 후, agent A와 private key ~ltk간의 관계를 의미하는 !Ltk($A, ~ltk)라는 fact를 생성했다. (exclamation mark !는 fact가 영구적이다라는 것을 의미한다.) 그리고, A와 그의 공개 키 pk(~ltk)를 연관짓는 !Pk($A, pk(~ltk)) fact를 생성한다.

해당 예제에서, 다음 규칙을 사용하여 적대자가 어떠한 공개키라도 얻게 할 수 있다. 필수적으로, 이 규칙은 공개 키 데이터베이스에서 엔트리를 읽고 built-in fact Out을 사용하여 네트워크로 공개 키를 전송한다.

rule Get_pk:
	[ !Pk(A, pubkey) ]
    -->
    [ Out(pubkey) ]

우리는 다음과 같은 규칙을 사용하여 long-term private key(장기 개인 키)의 동적 노출(dynamic compromise)를 설계할 수 있다. 직관적으로, 해당 규칙은 private-key 데이터베이스에서 항목을 엔트리를 읽고 적대자에게 그것을 전송하는 과정을 나타낸다. 이 규칙은 LtkReveal이라는 행동을 가지며, 이는 agent A의 long-term key가 노출되었다는 것을 의미한다. Action fact들은 fact와 유사하지만, 상태(State)에 남지 않고 오직 추적(Trace)에서만 나타난다. 보안 속성(The security properties)들은 이 추적들을 기반으로 정의되고, LtkReveal은 어떤 agent들이 노출되었는지를 판단하는데에 사용된다.

rule Reveal_ltk:
	[ !Ltk(A, ltk) ]
    --[ LtkReveal(A) ]->
    [ Out(ltk) ]

Modeling the protocol

Alice-and-Bob 모델을 돌이켜보자.

C -> S: aenc(k, pkS)
C <- S: h(k)

우리는 이것을 다음과 같은 3개의 규칙들로 모델링할 수 있다.

// Start a new thread executing the client role, choosing the server
// non-deterministically

rule Client_1:
	[ Fr(~k)					// choose fresh key
    , !Pk($S, pkS)				// lookup public-key of server
    ]				
    -->
    [ Client_1($S, ~k)			// Store server and key for next step of thread
    , Out(aenc(~k, pkS)) 		// Send the encrypted session key to the server
    ]		

rule Client_2:
	[ Client_1(S, k)			// Retrieve server and session key from previous step
    , In(h(k))					// Receive hased session key from network
    ]
    --[ SessKeyC(S, k) ]->		// State that the session key 'k'
    []							// was setup with server 'S'
    
    
// A server thread answering in one-step to a session-key 
// setup request from some client.

rule Serv_1:
	[ !Ltk($S, ~ltkS)						// lookup the private-key
    , In(request)							// receive a request
    ]
    --[ AnswerRequest($S, adec(request, ~ltkS)) ]->	  // Explanation below
    [ Out(h(adec(request, ~ltkS) ]			// Return the hash of 
    										// the decrypted request.

해당 코드에 대하여 몇 가지 설명이 필요한데,

• 첫 번째 규칙은 메시지를 전송하는 것이고, 두번째 규칙은 응답을 받는 것을 의미한다.
• 세 번째 규칙은 하나의 규칙으로 작성한 메시지를 수신하고 응답하는 서버를 의미한다.
• Tamarin은 C-style의 주석을 사용한다.
• 서버가 받은 세션-키 설정 요청을 행동(action)으로 기록(log)하여, 추후에 클라이언트의 인증 속성을 형식적으로 정의할 수 있도록 한다.

Modeling security properties

보안 속성들은 프로토콜의 실행의 action fact들의 추적들 위에서 정해진다.
우리는 평가할 2가지 보안 속성들을 가지고 있다.
Tamarin에서 평가될 보안 속성들은 lemmas로 표현된다.

첫 번째 평가할 속성은 클라이언트 시점으로부터 세션키의 기밀성(Secrecy)이다.
Client_session_key_secrecy라는 lemma는 클라이언트가 서버 S와 세션 키 k를 설정한 경우, 적대자가 k를 알게 되는 것은 오직 적대자가 서버의 long-term key를 노출시켰을 때만 가능하다는 것이다.

두 번째 lemma인 Client_auth는 클라이언트 인증을 의미한다.
이것은, 클라이언트가 서버 S와 설정한 모든 세션 키 k에 대하여, 반드시 요청에 대해 응답한 서버가 존재하거나 적대자가 이전에 S에 대한 long-term key 노출을 수행했다는 것을 의미한다.
(정상적인 상황에서는 클라이언트가 세션 키를 설정했을 때 반드시 대응하는 서버가 있어야 하며, 만약 그렇지 않은 경우 공격자가 서버의 장기 키를 노출시킨 경우에만 예외가 발생할 수 있음을 의미한다.)

lemma Client_session_key_secrecy:
" /* It cannot be that a */
  not(
    Ex S k #i #j.
      /* client has set up a session key 'k' with a server'S' */
      SessKeyC(S, k) @ #i
      /* and the adversary knows 'k' */
    & K(k) @ #j
    	/* without having performed a long-term key reveal on 'S'. */
    & not(Ex #r. LtkReveal(S) @ r)
  )
"


lemma Client_auth:
" /* For all session keys 'k' setup by clients with a server 'S' */
  ( All S k #i. SessKeyC(S, k) @ #i
    ==>
    	/* there is a server that answered the request */
    ( (Ex #a. AnswerRequest(S, k) @ a)
    	/* or the adversary performed a long-term key reveal on 'S'
    		before the key was setup. */
    | (Ex #r. LtkReveal(S) @ r & r < i)
    )
  )
"

우리는 또한 인증 속성을 더 강화하여 injective 인증 버전을 만들 수 도 있다.
우리의 공식화(formulation)는 일반적인 injective 인증보다 더 강력한 형태이다. 그 이유는 단순한 개수(counting)에 기반한 것이 아니라, 고유성(uniqueness)에 기반하기 때문이다. 대부분의 프로토콜이 injective 인증을 보장하는 경우, 적절한 새 데이터(fresh data)에 대한 합의가 이루어진다면, 고유성 주장도 증명할 수 있다.
이 속성은 Client_auth_injective lemma에서 볼 수 있다.

lemma Client_auth_injective:
	"	/* For all session keys 'k' setup by clients with a server 'S' */
    	( All S k #i. SessKeyC(S, k) @ #i
        	==>
            	/* there is a server that answered the request */
            (	(Ex #a. AnswerRequest(S, k) @ a
            	& ( All #j. SessKeyC(S, k) @ #j ==> #i = #j)
            )
            	/* or the adversary performed a long-term key reveal on 'S'
                before the key was setup. */
            |	(Ex #r. LtkReveal(S) @ r & r < i)
            )
        )
    "

우리의 lemma가 단순히 모델이 실행 불가능하기 때문에 공허하게(vacuously) 성립하는 것이 아님을 보장하기 위해서, 모델이 실제로 실행될 수 있고 완료될 수 있음을 보이는 실행 가능성(Excutability) lemma를 포함한다.
이 lemma는 일반적인 lemma와 동일한 형식으로 작성되지만,
exists-trace라는 키워드로 표현된다.
이 키워드는 이 lemma가 참이 되려면, 이 공식을 만족하는 실행(trace)이 하나라도 존재해야 한다.는 의미이다.
이는 이전의 lemma들과 대조되는데, 이전 lemma들은 모든 trace에서 성립해야 한다는 조건을 요구했다.
프로토콜을 모델링할 때, 이러한 존재성 증명(Existence proof)은 모델의 타당성을 확인하는 중요한 무결성 점검(sanity check)이 된다.

lemma Client_session_key_honest_setup:
	" Ex S k #i.
    	SessKeyC(S, k) @ #i
      & not(Ex #r. LtkReveal(S) @ r)
    "