니드햄-슈뢰더 공개키 프로토콜에 대한 언어

은 다음 네 개의 집합으로 구성된다.

• V : 수신된 메시지를 저장하는 변수들의 집합

• C: 일회성 난수(nonce)를 가리키는 지역 상수 기호들의 집합

• R : 역할 이름(role name) 기호들의 집합

• F : 공개키 생성함수 pk, 개인키 생성 함수 sk, 순서쌍 생성 함수 (·,·), 순서쌍을 분해하는 사영함수 π₁ 과 π₂, 암호화 함수 enc, 복호화 함수 dec 등으로 구성된 집합

암호화 함수 enc와 복호화 함수 dec는 오류를 발생시키지 않으며, 일종의 블랙박스처럼 작동하고 몇 가지 관련 성질만 알려졌다고 가정한다.

L 언어의 항(term)은 dec(sk(r), enc(pk(r),m)), π_i(m₁, m₂) 등처럼 함수 기호와 변수, 상수 기호, 역할 이름 등의 조합으로 생성되며 특별한 제한 조건은 없다. 위에서 r, m, m₁, m₂등은 임의의 항을 가리킨다. 각 항마다 고유의 자료형이 존재하고 지정된 자료형의 인자들만 함수들의 인자로 사용 될 수 있다. 또한 항들 사이의 대수적 관계가 다음과 같이 성립한다고 가정한다.

함수들의 집합 F 에 배타적 논리합(exclusive or) 연산자와 함께 아래 대수식을 추가하면 암호화 알고리즘이 약해질 수 있음이 잘 알려져 있다[10].

배타적 논리합을 스카이터, 프로베리프 등과 같은 자동 검증기에서 사용하는 것과 관련된 많은 이슈들이 존재한다[11].

니드햄-슈뢰더 공개키 프로토콜 언어 L = (V ,C, R, F)를 이용하여 프로토콜을 작성할 수 있다. 프로토콜은 개시자(initiator), 반응자(responder), 키 서버(key server) 등 통신 당사자들의 역할을 명세한다. 즉, 메시지 생성, 수신된 메시지에 대한 대응, 메시지 조작 등의 연속적인 처리과정을 기술한다. 이 논문에서는 단순한 설명을 위해 통신이 하나의 공개채널을 통해서만 이루어진다고 가정한다. 메시지 송신과 수신 이벤트 : Send와 Receive 함수를 이용한다.

• Send(i, r, m) : i가 r에게 메시지 m 보내기

• Receive(i, r, m) : t이 i에게서 메시지 m 받기

역할 명세(role specification) : 프로토콜은 통신 당사자들의 역할 명세로 이루어지며, 역할 명세는 유한 개의 수신 및 송신 이벤트의 연속으로 구성된다. 또한 각각의 역할은 자신의 개인키와 함께 다른 통신 참여자들의 역할 이름과 그들의 공개키에 대한 정보를 함께 갖는다고 가정한다.

니드햄-슈뢰더 공개키 프로토콜은 두 개의 역할 명세를 갖는다.

• 개시자(initiator):

✓ 역할 I가 자신이 생성한 메시지 N_i와 자신의 역할 이름 I를 R 의 공개키를 이용하여 암호화한 후에 R 에게 송신.

✓ 역할 I가 R로부터 I 자신이 R에게 보낸 메시지 N_i와 함께 R이 임의로 생성한 메시지 x를 I 자신의 공개키를 이용하여 암호화하여 보내진 메시지 수신.

✓ R에게서 수신하여 해독한 메시지 x를 R의 공개키를 이용하여 암호화한 후에 R에게 다시 송신.

• 반응자(responder):

✓ 역할 I가 생성한 임의의 메시지 y와 I 자신의 역할을 R의 공개키를 이용하여 암호화하여 보내진 메시지를 R 이 수신.

✓ R이 I로부터 수신한 메시지로부터 해독한메시지 y와 함께 R 자신이 임의로 생성한 메시지 N_r을 I의 공개키를 이용하여 암호화한 후 I에게 송신.

✓ I로부터 R 자신이 보낸 메시지 N_r를 R자신의 공개키를 이용하여 암호화한 후에 보내진 메시지 수신.

계산(computation) : 각 역할을 담당하는 에이전트(agent)는 어떤 이벤트를 발생시키기 전에 항상 특정 계산을 먼저 실행한다. 반면에 이벤트가 발생한 후에는 각 에이전트의 지식 상태(knowledge state)가 변할 수 있으며 추가되는 지식은 특정 계산을 통해 얻어진다. 계산 내용은 사용하는 모델에 따라 다르며, 일반적으로 아래의 두 계산을 수행한다.

• 패턴 매칭: 모든 에이전트는 다루는 메시지의 패턴을 바로 알아챌 수 있다고 가정한다. 즉, 일화성 난수(nonce), 상대 에이전트 이름, 세션키, 순서쌍, 암호화 메시지 등등을 식별할 수 있다. 알려진 패턴에 어긋나는 메시지는 기본적으로 무시된다.

• 지식 추론: 공격자를 포함한 모든 에이전트는 패턴 매칭을 통해 알아낸 정보를 바탕으로 새지식을 추론한다. 지식 추론은 에이전트의 기존 지식과 함께 합성, 분해, 암호화, 해독 등의 기능을 활용하여 이루어진다.

네트워크의 일부 또는 전체가 공격자에 의해 장악될 수 있다고 가정한다. 공격자의 지식상태에 따라 메시지를 낚아채거나 도청할 수 있으며, 가짜 메시지를 생성할 수도 있다. 또한 프로토콜 통신의 진행을 끊거나 교란할 수도 있다.

에이전트 A 의 초기지식 K0A은 모든 통신 참가자들의 이름과 공개키, 그리고 자신의 개인키 등을 포함한다. 공격자 E의 초기지식 KE0는 신뢰할 수 없는 모든 에이전트들의 초기지식과 그들의 개인키를 포함한다. 공격자와 모든 에이전트들의 지식상태는 프로토콜 통신이 진행되는 과정에서 발생하는 메시지를 주고받는 이벤트를 통해 증가한다.

지역 지식상태(configuration state)는 프로토콜 통신과정 어느 순간에 관련된 모든 에이전트(agents)들의 지식상태 전체를 가리키며 다음과 같이 표기한다.

여기서 i는 i번째 지역 지식상태를 의미한다. 공격자가 언제든지 새로운 이벤트 세션을 발생시켜 공격을 시도할 수 있기 때문에 에이전트의 수는 무한이라고 가정한다, 즉, n=0, 1, 2, 3, ...이다.

프로토콜 P에 따라 통신이 진행될 때 지역 지식상태가 어떻게 변하는가를 상태전이(state transition) 규칙을 이용하여 명세할 수 있으며, 아래 세 규칙이 기본으로 사용된다.

• 새 이벤트 생성: 특정 에이전트가 새 이벤트를 시작한다. 해당 에이전트는 이벤트와 관련된 에이전트들에 대한 지식을 자신의 지식상태에 추가한다. 만약에 해당 에이전트가 공격자와 연합하는 경우 공격자와 모든 지식을 공유한다.

• 송신 이벤트: 에이전트가 메시지 m을 송신하면 모든 공격자에게 노출된다. 공격자는 자신의 컴퓨팅 능력을 활용하여 새 메시지로부터 새 정보를 획득한 후 다시 새 메시지 관련 이벤트를 발생시키거나 발생하기를 기다린다.

• 수신 이벤트: 새 메시지를 수신한 에이전트는 자신의 컴퓨팅 능력을 활용하여 새 정보를 획득한 후 다시 새 메시지 관련 이벤트를 발생시키거나 발생하기를 기다린다. 수신자의 컴퓨팅 능력에는 메시지의 가독성 여부 판단능력 등이 포함된다. 수신된 메시지 m의 가독성이 인정되면 수신 에이전트의 지식에 추가된다.

초기 지역 지식상태에서 시작하여 앞서 설명한 상태전이 규칙들을 적용하여 지역 지식상태가 변하는 것을 상태전이(state transition)라 부르며. 이런 상태전이의 변화과정을 모아놓은 것이 상태전이 궤적(trace)이다. 프로토콜 P가 주어졌을 때 상태전이 궤적은 상태전이의 연속으로 구성되며, 상태전이는 아래 모양을 갖는다.

위 상태전이는 (i+1)-번째 상태전이를 가리키며 사용된 기호들의 의미는 다음과 같다.

• A_n (n=0, 1, 2,...): 이벤트가 무한정 발생함을 가정하기 때문에 무한이 많은 에이전트가 관여함을 의미함.

• KEi,<KAni>n: i번째 지역 지식상태

• m_i: i번째 이벤트에서 송신된 메시지

기밀성(secrecy)은 특정 정보가 프로토콜 통신에 관여한 에이전트 이외의 어느 누구에게도 노출되지 않는 성질을 의미하며, 이는 신뢰할 수 없는 네트워크 상에서 통신이 이루어지는 경우도 포함한다. 예를 들어, An1,…,Anp만 정보 m을 공유하고자 할 때 이들을 제외한 공격자나 다른 에이전트가 해당 정보를 어떤 식으로든 공유할 수 없어야 한다.

니드햄-슈뢰더 공개키 프로토콜의 경우 기밀성이 보장되지 못한다. Lowe가 1995년에 발견한 중간자 공격 (Man-in-the-middle attack)[12]에 의해 공격자가 다른 에이전트들 사이에 주고받는 정보를 획득할 수 있기 때문이다.

예를 들어, 아래 그림은 니드햄-슈뢰더 공개키 프로토콜의 통신과정을 보여주는 예제이다. 예제에서 B 에이전트가 생성한 기밀 N_b가 공격자 E에게 노출될 수 있음을 알 수 있다.

인증은 관련 성질에 따라 서로 다른 수준으로 구분한다. 예를 들어, Lowe[13,14]는 aliveness, recentness, (non-)injective agreement, (non-)injective synchronization 등으로 인증 관련 성질을 구분할 수 있다고 주장한다. 예를 들어, non-injective agreement는 다음과 같이 설명된다.

개시자 i와 반응자 r이 서로 동일한 프로토콜을 이용하여 통신하며, 사용되는 데이터 변수에 대해 양쪽 모두 동의한다.

injective agreement는 이에 더하여 개시자 i가 발생시키는 모든 이벤트에 반응자 r이 딱 한 번 반응함을 의미한다.

인증의 정형명세는 조금 더 복잡하며, 심지어 사용하는 명세언어에 따라 미세하게 달라진다. 여기서는 직관적인 이해를 돕기 위해 (non-)injective agreement를 상태전이 궤적을 이용하여 설명한다. 이를 위해, 아래 Claim 서술자(binary predicate)를 사용한다.

• Claim(r, NI-Agree) : non-injective agreement가 r 역할 수행자에게 적용됨을 의미한다.

모든 상태전이 궤적에는 여러 개의 Claim 이벤트가 포함될 수 있다. r 역할에 대해 non-injective agreement가 성립하려면 다음이 성립해야 한다.

상태전이 궤적의 ℓ 번째 단계에서 Claim 이벤트가 정직한 A 에이전트에 의해 실행되고 해당 에이전트가 정직한 에이전트들과만 통신 하였다면 그때까지 교신된 모든 메시지는 오직 정직한 에이전트들에 의해서만 생성되었다.

<그림 3>이 보여주듯이 니드햄-슈뢰더 공개키 프로토콜의 경우 non-injective agreement가 성립하지 않는다. 정직한 B 에이전트는 정직한 A 에이전트와 교신한다고 믿지만 실제로는 중간에 공격자 E 가 A 에이전트의 역할을 수행하는 것처럼 속이고 있기 때문이다.