Diffie Hellman Key Exchange Protocol Analysis

Proverif 프로그램을 이용한 Diffie Hellman Key Exchange 구현

https://bblanche.gitlabpages.inria.fr/proverif/manual.pdf

Proverif manual

Assignment I

Diffie-Hellman 키 교환 프로토콜 분석 및 구현

Oct 27, 2024

인공지능사이버보안학과

2020270103 임현성

목차

1. 서론

1.1 보고서의 목적

2. 기본 프로토콜 설계 (패시브 공격자)

2.1 프로토콜 개요

2.2 각 프로세스 설명

2.3 암호화 및 복호화

3. 디지털 서명 추가 및 액티브 공격자에 대한 대응

3.1 액티브 공격자 시나리오

3.2 디지털 서명 구현

3.3 각 프로세스의 서명 검증 과정

4. 코드 설명

4.1 패시브 공격자 대응 코드

4.2 액티브 공격자 대응 코드

5. ProVerif를 통한 검증 결과

5.1 패시브 공격자에 대한 검증

5.2 액티브 공격자에 대한 검증

1. 서론

1.1 목적

이 보고서의 목적은 Alice, Bob, Carol 세 사용자가 공동 비밀 키를 생성하여 안전하게 비밀 메시지를 공유할 수 있도록 Diffie-Hellman 키 교환 프로토콜을 설계하고 검증하는 데 있습니다.

사용자는 그룹 G에 대한 생성자 g를 공개적으로 선택하고, 각각 임의의 숫자 n0, n1, n2를 비공개적으로 선택합니다. 사용자가 공통 비밀 키에 대해 합의한 후, Alice는 비밀 키를 사용하여 비밀 메시지 s를 암호화한 후 Bob과 Carol에게 전달해야 합니다.

ProVerif를 활용하여 패시브 공격자와 액티브 공격자를 설정하고, 각각의 공격 모델에서 통신이 안전하게 이루어질 수 있는지 분석합니다.

2. 기본 프로토콜 설계 (패시브 공격자)

2.1 프로토콜 개요

프로토콜의 목적은 Alice, Bob, Carol이 공개 채널을 통해 공유 키를 생성하고, 이를 통해 비밀 메시지를 교환하는 것입니다.

패시브 공격자는 통신 내용을 도청할 수 있으나, 메시지나 키 값을 조작할 수 없습니다.

ProVerif에서는 기본적으로 제곱 연산을 위한 exp 함수를 제공하지만, 이 함수는 G 타입과 exponent 타입 간의 지수 연산만이 가능하기 때문에 세 사용자가 공통 비밀 키를 얻기 위해 추가적인 데이터 교환을 필요로 합니다.

구현 방법:

Alice, Bob, Carol은 서로 gx, gy, gz 값을 공유하고, 이를 통해 각각 필요한 중간 계산 값(gxy, gxz, gyz) 을 얻게 됩니다.

중간 계산 값은 exp 함수를 이용해 Alice, Bob, Carol의 n값과 계산되어 공유 키를 얻기 위한 값 (gxyz) 을 얻는데 사용됩니다.

이와 같은 단계별 연산 구조를 통해 최종 공유 키를 계산하게 되며, 이러한 과정이 구현된 이유는 ProVerif의 exp 함수에서 발생하는 제약을 극복하기 위함입니다.

Alice, Bob, Carol이 gxyz를 얻는 단계별 연산 과정

2.2 각 프로세스 설명

Alice의 프로세스:

Alice는 개인 지수 값 n0를 선택하고 gx 값을 계산하여 Carol과 Bob에게 전송합니다.

Carol에게 받은 gyz값을 사용해 공유 키를 계산합니다.

Bob의 프로세스:

Bob은 개인 지수 값 n1를 선택하고 gy 값을 계산하여 Carol에게 전송합니다.

Bob은 Alice에게 받은 gx값을 사용해 gxy를 계산하고 Carol에게 전송합니다.

Carol에게 받은 gxz 값을 사용해 공유 키를 계산합니다.

Carol의 프로세스:

Carol은 개인 지수 값 n2를 선택하고 gz 값을 계산합니다.

Alice와 Bob에게 받은 gx, gy값을 통해 gxz, gxy를 계산하고 Alice와 Bob에게 전송합니다.

Bob에게 받은 gxy값을 사용해 공유 키를 계산합니다.

2.3 암호화 및 복호화

암호화 과정:

Alice는 공유 키를 사용해 비밀 메시지를 암호화하고, 이를 Bob과 Carol에게 전송합니다.

암호화 함수 enc와 복호화 함수 dec가 이 과정에서 사용되며, 공유 키를 키 값으로 하여 비밀 메시지를 전송합니다.

복호화 과정:

Bob과 Carol은 공유 키를 사용하여 암호화된 메시지를 복호화하여 비밀 메시지를 확인합니다.

3. 디지털 서명 추가 및 액티브 공격자에 대한 대응

3.1 액티브 공격자 시나리오

액티브 공격자는 메시지나 키 교환 과정을 조작할 수 있는 능력을 가집니다.

이 경우, 메시지 변조와 키 값 위조 등의 공격이 가능하므로, 단순 암호화만으로는 통신의 무결성을 보장할 수 없습니다.

따라서 각 참여자가 디지털 서명을 사용하여 메시지 송신자에 대한 무결성을 입증할 수 있도록 합니다.

3.2 디지털 서명 구현

비공개 키와 공개 키: Alice, Bob, Carol 각각의 개인 키와 공개 키를 정의하여, 이를 통해 서명 및 검증을 수행합니다.

서명과 검증 함수:

sign 함수는 메시지를 개인 키로 서명하여, 해당 메시지가 정상적인 송신자에 의해 송신되었음을 증명합니다.

verify 함수는 서명된 메시지를 공개 키로 검증하여 서명자가 누구인지 식별하고, 메시지가 변조되지 않았음을 확인합니다.

3.3 각 프로세스의 서명 검증 과정

프로세스

Alice, Bob, Carol이 보내는 모든 데이터에 서명 함수를 적용합니다.

Alice, Bob, Carol이 데이터를 받는 경우, 해당 데이터를 공개 키로 검증하여 서명자를 식별하고 메시지의 무결성을 확인합니다.

서명을 통해 각 참여자는 전달받은 메시지가 변조되지 않았고, 신뢰할 수 있는 참여자로부터 온 것임을 검증합니다.

4. 코드 설명

4.1 패시브 공격자 대응 코드

공격자 설정:

이 코드에서는 패시브 공격자만을 가정하고 있습니다. 공격자는 통신을 도청할 수 있지만 메시지나 값을 변조할 수 없습니다.

따라서 코드에서 서명이나 검증 기능이 구현되지 않았으며, 각 참여자 간의 키 교환과 암호화된 메시지 전송만이 구현됩니다.

Passive 코드에 사용된 요소 정리

1. 채널 정의

channel_ab: Alice와 Bob 사이의 통신을 위한 채널.

channel_ac: Alice와 Carol 사이의 통신을 위한 채널.

channel_bc: Bob과 Carol 사이의 통신을 위한 채널.

각 채널은 참여자 간의 데이터 전송을 위해 사용되며, out과 in 구문을 통해 특정 데이터를 전송하고 수신하는 역할을 수행합니다.

2. 함수 정의

enc(bitstring, G): bitstring:

비밀 메시지를 암호화하는 함수입니다. G 타입(공유 키)을 사용하여 메시지(bitstring)를 암호화하고, 암호화된 bitstring을 반환합니다.

dec(bitstring, G): bitstring:

암호화된 메시지를 복호화하는 함수입니다. 공유 키(G 타입) 로 복호화하여 원본 메시지(bitstring) 를 복원합니다.

reduc 규칙을 통해 암호화와 복호화가 서로 상호작용하여 원본 메시지를 복구할 수 있도록 설정됩니다.

exp(G, exponent): G:

지수 연산 함수로, 공개 생성자 G와 개인 지수(exponent 타입)를 사용해 G 타입 값을 생성합니다.

각 참여자는 exp 함수로 생성된 값을 통해 공유 키를 도출하는 계산을 수행합니다.

3. 생성자 및 상수

g: G:

Alice, Bob, Carol이 사용하는 공개 생성자입니다. 이 값을 기반으로 개인 지수와 연산하여 공유 키를 생성합니다.

ok: bitstring, not_ok: bitstring:

메시지 검증을 위한 상수로, 메시지가 정상적으로 복호화되었음을 나타냅니다.

4. 변수

개인 지수 변수:

n0: Alice의 개인 지수입니다.

n1: Bob의 개인 지수입니다.

n2: Carol의 개인 지수입니다.

공유 키 계산을 위한 변수:

gx, gy, gz: 각 참여자가 공개 생성자 g와 자신의 개인 지수를 제곱 연산하여 얻는 값들입니다.

gxy, gxz, gyz: 참여자 간의 공유 키 계산에 필요한 중간 결과로, 최종적으로 개인지수와 제곱 연산하여 shared_key를 얻는데 사용됩니다.

shared_key: 최종적으로 도출되는 공유 키로, Alice, Bob, Carol이 각자의 개인 지수와 다른 참여자로부터 받은 값을 조합해 계산한 값입니다.

비밀 메시지 변수:

s: Alice가 Bob과 Carol에게 전달할 비밀 메시지로, 공유 키를 사용해 암호화된 후 전송됩니다.

프로세스 설명:

Alice:

Alice는 개인 지수 값 n0를 생성하고, 이를 사용해 gx 값을 계산합니다.

Alice는 gx를 Bob과 Carol에게 각각 전송합니다.

Carol로부터 전달받은 gyz 값을 사용해 공유 키를 계산합니다.

공유 키를 통해 비밀 메시지를 암호화하여 Bob과 Carol에게 전송합니다.

Bob:

Bob은 개인 지수 값 n1를 생성하고, 이를 사용해 gy 값을 계산하여 Carol에게 전송합니다.

Alice로부터 전달받은 gx 값을 사용해 gxy 값을 계산하고 Carol에게 전송합니다.

Carol로부터 전달받은 gxz 값을 사용해 공유 키를 계산합니다.

Alice로부터 전달받은 암호화된 비밀 메시지를 복호화하여 확인합니다.

Carol:

Carol은 개인 지수 값 n2를 생성하고, 이를 사용해 gz값을 계산합니다.

Alice와 Bob으로부터 각각 gx, gy 값을 받고 gxz, gyz 값을 계산해 Alice와 Bob에게 각각 전송합니다.

Bob으로부터 전달받은 gxy 값을 사용해 공유키를 계산합니다.

Alice로부터 전달받은 암호화된 비밀 메시지를 복호화하여 확인합니다.

4.2 액티브 공격자 대응 코드

공격자 설정:

이 코드에서는 액티브 공격자를 가정하여, 공격자가 통신을 조작할 수 있는 상황을 방어하기 위해 디지털 서명 및 검증 기능을 추가하였습니다.

액티브 코드에서 추가된 요소들

1. 함수

sign(bitstring, privKey): bitstring:

bitstring 타입의 메시지를 개인 키(privKey)로 서명하여 전송하는 함수입니다.

각 참여자는 이 함수를 통해 자신이 보낸 메시지가 변조되지 않았음을 증명할 수 있습니다.

verify(bitstring, bitstring, pubKey): bitstring:

서명된 메시지와 공개 키(pubKey)를 입력받아 메시지의 무결성을 확인하는 함수입니다.

검증이 성공하면 ok 값을 반환하고, 실패 시 not_ok 값을 반환합니다.

to_bitstring(G): bitstring:

G 타입 값을 bitstring으로 변환하는 함수로, 서명과 검증에 필요한 값들을 bitstring 타입으로 변환해 서명할 수 있도록 합니다.

exp 함수의 결과를 sign 함수에 입력할 수 있게 해주는 역할을 합니다.

2. 상수

ok: bitstring:

검증 성공을 나타내는 상수로, verify 함수가 서명을 성공적으로 검증했을 때 반환합니다.

not_ok: bitstring:

검증 실패를 나타내는 상수로, verify 함수가 서명을 검증하지 못했을 때 반환합니다.

3. 개인 키와 공개 키

개인 키:

각 참여자의 개인 키로, 디지털 서명을 생성하는 데 사용됩니다. Alice, Bob, Carol은 이 개인 키를 사용해 전송하는 메시지를 서명하여 메시지의 무결성을 입증합니다.

공개 키:

각 참여자의 공개 키로, 서명을 검증하는 데 사용됩니다. Alice, Bob, Carol은 서로의 공개 키를 사용해 수신한 메시지의 서명을 검증하여, 해당 메시지가 신뢰할 수 있는 참여자로부터 온 것인지 확인합니다.

프로세스 설명 (Carol 프로세스) :

디지털 서명: Alice, Bob, Carol이 주고받는 모든 통신에 디지털 서명을 생성하고 검증합니다.

검증: 데이터를 수신할 때마다 서명을 검증하고 메시지의 출처가 불분명할 경우 프로세스를 종료합니다.

5. ProVerif를 통한 검증 결과

5.1 패시브 공격자에 대한 검증

검증 과정:

ProVerif에서 패시브 공격자 설정을 통해 통신을 도청할 수 있는 상황을 시뮬레이션하였습니다.

ProVerif의 결과로 공격자가 비밀 메시지와 공유 키에 접근하지 못함을 확인했습니다. 그러나, 패시브 공격자는 메시지를 조작하거나 훼손하지 않기 때문에 프로토콜의 무결성이 지켜졌는지 알 수 없습니다.

검증 결과:

Alice, Bob, Carol 간의 공유 키가 생성되었으며, 비밀 메시지를 성공적으로 복호화 했습니다.

5.2 액티브 공격자에 대한 검증

목적: 액티브 공격자 모델에서, 디지털 서명이 있는 경우 공격자가 통신을 조작하더라도 메시지의 무결성과 신원이 유지되는지를 검증합니다.

검증 과정:

ProVerif에서 액티브 공격자 설정을 통해 공격자가 통신을 도청하고 조작할 수 있는 상황을 시뮬레이션하였습니다.

sign과 verify 함수를 통해 참여자들이 각 메시지와 키 교환에 서명을 수행하며, 각 서명이 유효한지 확인하였습니다.

각 메시지 전송 및 검증 과정에서 공격자가 서명된 메시지나 키 값을 변조할 수 없음을 검증하였고, 공격자가 변조 시도 시 올바르지 않은 서명으로 검증이 실패함을 확인하였습니다.

검증 결과:

디지털 서명을 추가한 프로토콜은 액티브 공격자 모델에서 통신 무결성을 유지했습니다.

ProVerif 결과에 따르면 공격자가 메시지를 변조하더라도 검증 과정에서 이를 식별할 수 있으므로, 프로토콜의 무결성이 보장됩니다.

3 Channels, Signature X

free channel_ab: channel.
free channel_ac: channel.
free channel_bc: channel.

type G.
type exponent.

set attacker = passive.

fun enc(bitstring, G): bitstring.
reduc forall x: bitstring, y: G; dec(enc(x, y), y) = x.

const g: G.
fun exp(G, exponent): G.
equation forall x: exponent, y: exponent; exp(exp(g, x), y) = exp(exp(g, y), x).

free s: bitstring [private].
query attacker(s).

(* Alice 프로세스 *)
let p0 = new n0: exponent;
let gx = exp(g, n0) in
out(channel_ac, gx);

in(channel_ac, gyz: G);
let shared_key = exp(gyz, n0) in

out(channel_ab, gx);

let encrypted_message = enc(s, shared_key) in
out(channel_ab, encrypted_message);
out(channel_ac, encrypted_message).

(* Bob 프로세스 *)
let p1 = new n1: exponent;
let gy = exp(g, n1) in

out(channel_bc, gy);

in(channel_bc, gxz: G);
let shared_key = exp(gxz, n1) in

in(channel_ab, gx: G);
let gxy = exp(gx, n1) in

out(channel_bc, gxy);

in(channel_ab, encrypted_message: bitstring);
let s_bob = dec(encrypted_message, shared_key).

(* Carol 프로세스 *)
let p2 = new n2: exponent;
let gz = exp(g, n2) in

in(channel_ac, gx: G);
let gxz = exp(gx, n2) in

in(channel_bc, gy: G);
let gyz = exp(gy, n2) in

out(channel_ac, gyz);

out(channel_bc, gxz);

in(channel_bc, gxy: G);
let shared_key = exp(gxy, n2) in

in(channel_ac, encrypted_message: bitstring);
let s_carol = dec(encrypted_message, shared_key).

process p0 | p1 | p2

3 Channel, Signature O

free channel_ab: channel.
free channel_ac: channel.
free channel_bc: channel.

type G.
type exponent.

set attacker = active.

fun enc(bitstring, G): bitstring.
reduc forall x: bitstring, y: G; dec(enc(x, y), y) = x.

const g: G.
fun exp(G, exponent): G.
equation forall x: exponent, y: exponent; exp(exp(g, x), y) = exp(exp(g, y), x).

type privKey.
type pubKey.

fun to_bitstring(G): bitstring.
fun sign(bitstring, privKey): bitstring.
fun verify(bitstring, bitstring, pubKey): bitstring.

const ok: bitstring.
const not_ok: bitstring.

const alice_priv: privKey [private].
const alice_pub: pubKey.
const bob_priv: privKey [private].
const bob_pub: pubKey.
const carol_priv: privKey [private].
const carol_pub: pubKey.

free s: bitstring [private].
query attacker(s).

(* Alice 프로세스 *)
let p0 = new n0: exponent;
let gx = exp(g, n0) in
let signed_gx_to_carol = sign(to_bitstring(gx), alice_priv) in
out(channel_ac, gx);
out(channel_ac, signed_gx_to_carol);

in(channel_ac, gyz_from_carol: G);
in(channel_ac, signed_gyz_from_carol: bitstring);
if verify(to_bitstring(gyz_from_carol), signed_gyz_from_carol, carol_pub) = ok then
let shared_key = exp(gyz_from_carol, n0) in

let signed_gx_to_bob = sign(to_bitstring(gx), alice_priv) in
out(channel_ab, gx);
out(channel_ab, signed_gx_to_bob);

let encrypted_message = enc(s, shared_key) in
let signed_encrypted_message = sign(encrypted_message, alice_priv) in
out(channel_ab, encrypted_message);
out(channel_ab, signed_encrypted_message);
out(channel_ac, encrypted_message);
out(channel_ac, signed_encrypted_message)
else
0.

(* Bob 프로세스 *)
let p1 = new n1: exponent;
let gy = exp(g, n1) in
let signed_gy_to_carol = sign(to_bitstring(gy), bob_priv) in
out(channel_bc, gy);
out(channel_bc, signed_gy_to_carol);

in(channel_bc, gxz_from_carol: G);
in(channel_bc, signed_gxz_from_carol: bitstring);
if verify(to_bitstring(gxz_from_carol), signed_gxz_from_carol, carol_pub) = ok then
let shared_key = exp(gxz_from_carol, n1) in

in(channel_ab, gx_from_alice: G);
in(channel_ab, signed_gx_from_alice: bitstring);
if verify(to_bitstring(gx_from_alice), signed_gx_from_alice, alice_pub) = ok then
let gxy = exp(gx_from_alice, n1) in
let signed_gxy_to_carol = sign(to_bitstring(gxy), bob_priv) in
out(channel_bc, gxy);
out(channel_bc, signed_gxy_to_carol);

in(channel_ab, encrypted_message: bitstring);
in(channel_ab, signed_encrypted_message: bitstring);
if verify(encrypted_message, signed_encrypted_message, alice_pub) = ok then
let s_bob = dec(encrypted_message, shared_key) in 0
else
0
else
0
else
0.

(* Carol 프로세스 *)
let p2 = new n2: exponent;
let gz = exp(g, n2) in
in(channel_ac, gx: G);
in(channel_ac, signed_gx_from_alice: bitstring);
if verify(to_bitstring(gx), signed_gx_from_alice, alice_pub) = ok then
let gxz = exp(gx, n2) in
let signed_gxz_to_bob = sign(to_bitstring(gxz), carol_priv) in
out(channel_bc, gxz);
out(channel_bc, signed_gxz_to_bob);

in(channel_bc, gy: G);
in(channel_bc, signed_gy_from_bob: bitstring);
if verify(to_bitstring(gy), signed_gy_from_bob, bob_pub) = ok then
let gyz = exp(gy, n2) in
let signed_gyz_to_alice = sign(to_bitstring(gyz), carol_priv) in
out(channel_ac, gyz);
out(channel_ac, signed_gyz_to_alice);
in(channel_bc, gxy: G);
in(channel_bc, signed_gxy_from_bob: bitstring);
if verify(to_bitstring(gxy), signed_gxy_from_bob, bob_pub) = ok then
let shared_key = exp(gxy, n2) in
in(channel_ac, encrypted_message: bitstring);
in(channel_ac, signed_encrypted_message: bitstring);
if verify(encrypted_message, signed_encrypted_message, alice_pub) = ok then
let s_carol = dec(encrypted_message, shared_key) in 0
else
0
else
0
else
0
else
0.

process p0 | p1 | p2