Blog

2018.10.26

LINE のグループメッセージプロトコルの ProVerif によるモデル化と検証

概要

メッセンジャーサービス LINE の暗号化通信プロトコルを ProVerif を用いてモデル化し，安全性を検証したという論文 [1] を読んだことをきっかけに，そこで扱われていなかった E2EEP-1:N (グループメッセージプロトコル) の ProVerif によるモデル化と，その安全性の検証を試みました．

具体的には，論文 [1] とホワイトペーパー [2] を読み，[2] の E2EEP-1:N プロトコルの説明を元にシーケンス図を作成し，それを元に ProVerif のモデルを作成しました． このモデルを検証した結果，

  • メッセージの秘匿性: 成立
  • 認証性(injective): 不成立 (ProVerifのモデルはリプレイ攻撃に対して脆弱)
  • 認証性(non-injective): 成立

という結果を得ました．

作成した ProVerif のスクリプトは，こちらから download できます: LINE_E2EEP1n.pv

注意: この結果は，[2] で説明されている内容のみに基づき作成した ProVerif のモデル上で成立するものであり，実際のプロトコルにおいても同様に成立かどうかは不明であることに注意してください．

はじめに

こんにちは，エンジニアの山田です．今回，メッセージングサービスとしてポピュラーな LINE で使われている暗号化通信プロトコルを ProVerif でモデル化し，その安全性を検証したという論文 [1] を読む機会がありました．

LINE の暗号化通信プロトコルは，ホワイトペーパー [2] で説明されていて，TEP, E2EEP-1:1, E2EEP-1:N, VoIP End-to-End Encryption の4つのプロトコルが示されています:

  • TEP: Client-to-Server Transport Encryption Protocol

    LINE サービスのクライアントとサーバとの間の通信を保護するために使用されるプロトコル

  • E2EEP: Message End-to-End Encryption ([2]では Letter Sealing と呼ばれている)

    LINE サービスのクライアント間の通信を保護するために利用されるプロトコル．以下の2種類のプロトコルから構成される:

    • E2EEP-1:1: 1:1 Message Encryption

      1:1のクライアント同士のメッセージ通信を保護するために利用されるプロトコル

    • E2EEP-1:N: 1:N (group) Message Encryption

      複数のクライアントからなるグループ内のメッセージ通信を保護するために利用されるプロトコル

  • VoIP End-to-End Encryption

    1:1のクライアント同士の音声通話を保護するために利用されるプロトコル

[1]では，これらのうち TEP と E2EEP-1:1 についてProVerif でモデル化し，検証しています． 検証の内容に気になる点がありましたが，今回はそこには注目せず，[1]で扱われていないプロトコルのうち，グループ内のメッセージ通信のための E2EEP-1:N プロトコルについて， ProVerif によるモデル化と検証に挑戦してみることにしました．

以降では，ProVerif についての知識を前提に説明を進めます． ProVerif に関する情報は，開発者らによるウエブページ [3] にまとまっていますので，必要に応じで参照してください．

ホワイトペーパーの説明からシーケンス図を作成

まず，E2EEP-1:N プロトコルがどうなっているのか確認します．

ホワイトペーパー [2] の第4.3節にE2EEP-1:N プロトコルの説明がありますが，式が少なく図は使われず主に文章で説明されているため，そこから直接 ProVerif のモデルを作成するのは難しいと考えました． そこで，一旦，この説明を読んで理解した内容を元にシーケンス図を作成し，次に，そのモデルを元に ProVerif のモデルを作成することにしました．

ここでは，[2] の第4.3節を読んで理解した E2EEP-1:N プロトコルを，以下の5つのシーケンス図として示します:

  1. ユーザの鍵ペアの作成，公開鍵の登録
  2. グループ共通鍵の作成・登録
  3. グループ共通鍵を取得
  4. グループメッセージを送信
  5. グループメッセージを受信

1. ユーザの鍵ペアの作成，公開鍵の登録

全ての LINE メッセンジャーサービスの利用者は， ECDH 鍵ペアを生成し，公開鍵をサーバに登録し，秘密鍵を端末内に保持します．

E2EEP1n-01.png

LINE メッセンジャーサービスの利用者がサービスの利用を開始する際，サービスの利用者(ここでは仮にメンバー A とします)が利用するクライアントアプリケーションは， ECDH 鍵ペア を生成し，公開鍵 () をサーバ (MessagingServer) へ送信し，秘密鍵 () を端末内の安全な領域に保存します．

サーバは，受け取った公開鍵を保持します． [2] では，公開鍵の管理方法は説明されていません． 今回は，図のように PublicKeyTable テーブルを利用することとしました．

端末とサーバ間の通信は，TEP プロトコルで保護されます．

この処理は，E2EEP-1:1プロトコルの一部です．

2. グループ共通鍵の作成・登録

グループが作成された場合，グループ共通鍵が生成され，グループのメンバー全てに共有されます．

E2EEP1n-02.png

複数のユーザーから成るグループ（ここでは，仮にメンバー A, B, C から成るグループ “G”とします) が作成された場合，メンバーの一人(仮に A)が利用するクライアントアプリケーションは，ECDH鍵ペアを生成し，秘密鍵をグループ共通鍵 () とします(公開鍵は使用しません)．

次に，他のメンバー (メンバー B, C) の公開鍵をサーバから取得し (それぞれ , )，自分の秘密鍵と組み合わせて，グループ共通鍵を暗号化するための共通鍵を生成します(それぞれ , )．

続いて，生成した共通鍵でグループ共通鍵を暗号化し (それぞれ , )，サーバに送信します．

これらを受け取ったサーバは，暗号化されたグループ共通鍵それぞれを保持します． [2] では，グループ鍵の管理方法は説明されていません． 今回は，図のように GroupSharedKeyTable テーブルを利用することとしました．

これらの処理は，グループ作成時ではなく，グループ作成後，あるメンバーが最初にグループメッセージを送信しようとした時点で，そのメンバーのクライアントアプリケーションにより行われると [2] で説明されています．

3. グループ共通鍵を取得

グループメッセージを送信する際，送信者がグループ共通鍵を持たない場合は，それをサーバから取得します．

E2EEP1n-03.png

グループのあるメンバー(仮にメンバー B とします)が，グループのメンバー達へメッセージを送信する際にグループ共通鍵 () を保持していなかった場合，以下の手順に従い，グループ共通鍵を取得します． すでにグループ共通鍵を保持している場合は，その鍵を使います(以下の処理は行いません)．

グループ共通鍵取得のためには，まずサーバから，グループ共通鍵作成者(仮にメンバーAとする)のIDと自分の共通鍵 () で暗号化されたグループ共通鍵 () を取得します．

次に，グループ共通鍵作成者の公開鍵 () をサーバから取得します．

ここで，取得した公開鍵と自分の秘密鍵 () とから，グループ共通鍵作成者と自分の間の共通鍵 () を計算し，この鍵を用いて暗号化されたグループ共通鍵を復号し，グループ共通鍵 ()を取得します．

4. グループメッセージを送信

グループ共通鍵を元に計算した 共通鍵 やIV (初期化ベクトル)を使用して，送信メッセージを暗号化した暗号化メッセージと，そのメッセージ認証コードを，グループメンバーそれぞれに送信します．

E2EEP1n-04.png

グループメッセージの送信者は，まずグループ共通鍵 () と自分の公開鍵()からグループ共通シークレット () を計算します．

次に，乱数 () を生成し，それとグループ共通シークレットから 共通鍵 () と IV () を計算します．

続いて，共通鍵と IV を用いて， 送信するメッセージ () を暗号化して暗号化メッセージ () を生成し，そのメッセージ認証コード()を計算します．

最後に，暗号化メッセージとメッセージ認証コードと，その他の情報をひとまとめにしてグループのメンバーそれぞれに送信します．

5. グループメッセージを受信

あるメンバーがグループメッセージを受信したら，必要に応じてサーバからグループ共通鍵を取得し，それを元に暗号鍵やIVを計算し，それらを用いて受け取った暗号メッセージからメッセージ認証コードを計算して，受け取ったメッセージ認証コードとの一致を確認し，一致した場合は暗号メッセージを復号します．

E2EEP1n-05.png

グループメッセージを受信した場合，受信者がグループ共通鍵 () を持っていない場合は，「グループ共通鍵を取得」処理と同じ手順で，サーバからグループ共通鍵を取得します．

次に，メッセージ送信者(ここでは仮にメンバー B)の公開鍵 () をサーバから取得し，それとグループ共通鍵とから，グループ共通シークレット () を計算します．

続いて，グループ共通シークレットと，受信したメッセージに含まれる乱数 () とから，共通鍵 () を計算します．

また，受信したメッセージに含まれる暗号化されたメッセージ () と共通鍵から，メッセージ認証コード () を計算し，これが受信したメッセージに含まれるメッセージ認証コード ()と一致するか確認します．

メッセージ認証コードが一致した場合，グループ共通シークレットと乱数からIV ()を計算し，それと共通鍵を用いて暗号化されたメッセージを復号し，平文のメッセージ () を得ます．

シーケンス図から ProVerif のモデルを作成

次に，前節で説明した E2EEP-1:N プロトコルのシーケンス図を元に， ProVerif のモデルを作成します．

ProVerif のモデル記述言語の制約や，モデルの複雑化を避ける目的で，前節で説明したシーケンス図によるモデルを以下のように変更した ProVerif のモデルを作成しました:

  • 任意の数のメンバーから成るグループを ProVerif で扱うことが難しいため，グループのメンバーを3名に限定．
  • 同様に，ありとあらゆる状況を表現するモデルを扱うことが難しいため，以下のシナリオに限定:
    • Member A がグループを作成，Member B はグループメッセージを送信，それを Member A と Member C が受信

    E2EEP1n-activity.png

  • 簡単のため， Member A, …, Member C と MessagingServer 間の通信は，共通鍵暗号でモデル化(本来はTEP)．
  • 各メンバーが鍵を登録する前に攻撃者が鍵を登録してしまう動作を避けるため，攻撃者は MessagingServer へ鍵を登録できないように制限．

作成した ProVerif のスクリプトはこちらです (概要で示したものと同一です): LINE_E2EEP1n.pv

以降では，作成した E2EEP-1:N プロトコルの ProVerif のモデルを説明します．

暗号プリミティブと関数の定義

[2] の E2EEP-1:N プロトコルの定義の中で使われている暗号プリミティブは，ECDH, AESCBC, AESECB, SHA256, 不明プリミティブ(グループ共通鍵暗号化・復号用)であり，関数は xor，[0:15]，[16:31] (subbitstring)です． これらと関連するデータ型，データ型の変換関数の ProVerif での定義を以下に示します:

(* Rules for ECDH key exchange *)
type G.                                        (* type of generator *)
type scalar.                                   (* type of scalar *)
type basis.                                    (* type of base points *)
fun Ggen(basis):G.                             (* convert base point to generator *)
fun sca(scalar,G):G.                           (* scalar multiplication *)
equation forall a:scalar, b:scalar, P:basis;
  sca(a,sca(b,Ggen(P)))=sca(b,sca(a,Ggen(P))). (* commutativity *)

(* Types *)
type key.
type iv.

(* Rules for AES-CBC *)
fun senccbc(bitstring,key,iv):bitstring.                              (* encryption function *)
reduc forall m:bitstring, k:key, i:iv; sdeccbc(senccbc(m,k,i),k,i)=m. (* decryption function *)

(* Rules for AES-ECB *)
fun sencecb(bitstring,key):bitstring.                       (* encryption function *)
reduc forall m:bitstring, k:key; sdececb(sencecb(m,k),k)=m. (* decryption function *)

(* Rules for SHA256 *)
fun Hash(bitstring):bitstring. (* hash function *)

(* Rules for unknown algorithm to encrypt/decrypt group shared key *)
fun ENC(scalar, G):bitstring.
reduc forall k:G, x:scalar; DEC(ENC(x, k), k) = x.

(* Rules for XOR *)
fun xor(bitstring,bitstring):bitstring.
equation forall x:bitstring, y:bitstring; xor(xor(x,y),y)=x.
equation forall x:bitstring; xor(x,xor(x,x))=x.
equation forall x:bitstring; xor(xor(x,x),x)=x.
equation forall x:bitstring, y:bitstring; xor(y,xor(x,x))=y.
equation forall x:bitstring, y:bitstring; xor(xor(x,y),xor(x,x))=xor(x,y).
equation forall x:bitstring, y:bitstring; xor(xor(x,y),xor(y,y))=xor(x,y).

(* Rules for subbitstring -- not explaned on the paper -- *)
fun breakf(bitstring):bitstring.
fun breakb(bitstring):bitstring.

(* Rules for type conversion *)
fun ToKey(bitstring):key. (* convert bitstring type to key type *)
fun ToIV(bitstring):iv.   (* convert bitstring type to iv type *)

この定義は， [1] で示されている ProVerif のスクリプトの暗号プリミティブやデータ型等の定義を，一部修正したものとなっています．

定数等の定義

E2EEP-1:N の ProVerif のモデルを定義する際に定数として，楕円曲線のベースポイント(J), コンテキスト(Key, IV), E2EEP-1:N のメッセージのメタ情報(ver, contentType)，メッセージ送受信のために使用するチャネル(c), グループのIDを共有するた目のチャネル(c_pr), 送受信される平文のメッセージ(M)を使用し，データ型として，乱数(coins), ID(ID), メッセージのメタ情報(version, ContentType)を使用します:

(* Types *)
type coins.
type ID.
type version.
type ContentType.

(* Constants *)
const J:basis[data].
const Key:bitstring[data].
const IV:bitstring[data].
const ver:version[data].
const contentType:ContentType[data].

(* Declaration of channel and secret *)
free c:channel.             (* channel *)
free c_pr:channel[private]. (* private channel to share groupKeyID *)
free M:bitstring[private].  (* client's secret information *)

サーバの定義

サーバは，チャネルを通してメッセージをやりとりし，鍵の登録・参照を行います．

サーバとクライアントとの間の通信は TEP で保護されますが，サーバを ProVerif でモデル化するにあたりモデルが複雑になることを避けるため，TEP を共通鍵暗号で置き換えたモデルとしました:

(* Abstract TEP model *)
type TEPSessionKey.

fun TEPENC(TEPSessionKey, bitstring): bitstring.
reduc forall k:TEPSessionKey, x:bitstring; TEPDEC(k, TEPENC(k, x)) = x.

const Client1TEPSessionKey: TEPSessionKey[private].
const Client2TEPSessionKey: TEPSessionKey[private].
const Client3TEPSessionKey: TEPSessionKey[private].
const AttackerTEPSessionKey: TEPSessionKey.

メッセージングサーバとやりとりされるメッセージは，コマンドと，付随するデータから構成されます． コマンドは以下のような定数として定義しました:

(* Messaging Server *)
type MessagingServerMessageType.
const RegisterPublicKey: MessagingServerMessageType.
const ResponseRegisterPublicKey: MessagingServerMessageType.
const QueryPublicKey: MessagingServerMessageType.
const ResponsePublicKey: MessagingServerMessageType.

const RegisterGroupKey2: MessagingServerMessageType.
const ResponseGroupKeyID: MessagingServerMessageType.
const QueryGroupKey: MessagingServerMessageType.
const ResponseGroupKey: MessagingServerMessageType.

LINEの利用者の公開鍵，グループ共通鍵の管理は，ProVerif のモデルではテーブルを利用して行います． 公開鍵はテーブル publickey_table に，利用者の ID と鍵の組みとして保持します． また，グループ共通鍵は，鍵作成者と鍵受け渡し先の利用者の共通鍵で暗号化された状態で管理され，テーブル groupkey_table に，鍵作成者のID, 鍵受け渡し先の利用者のID, 暗号化された鍵, グループのIDの組みとして保持します:

table publickey_table(ID, G).
table groupkey_table(ID, ID, bitstring, ID). (* (encryptedFor, encryptedBy, groupKeyEncrypted, groupKeyID) *)

サーバは，サブプロセス MessagingServer として定義します． チャネル c から暗号化されたリクエストメッセージを受け取り， それを復号し，コマンドの種類に応じた処理を実行し，結果を暗号化してチャネル c を通して返します． 暗号化には，TEPの代わりに共通鍵暗号を使用しています:

let MessagingServer_register(msg:bitstring, sessionKey:TEPSessionKey) =
  let decrypted: bitstring = TEPDEC(sessionKey, msg) in
  let (=RegisterPublicKey, id:ID, pubKey:G, nonce:coins) = decrypted in
  (
    get publickey_table(=id, k:G) in 0 (* already registered *) else
    (
      insert publickey_table(id, pubKey);
      out(c, TEPENC(sessionKey, (ResponseRegisterPublicKey, id, nonce)))
    )
  )
  else let (=RegisterGroupKey2, groupKeyID:ID, encryptedBy:ID, (encryptedFor1:ID, groupKeyEncrypted1:bitstring), (encryptedFor2:ID, groupKeyEncrypted2:bitstring), nonce:coins) = decrypted in
  (
    get groupkey_table(=encryptedFor1, =encryptedBy, k1:bitstring, =groupKeyID) in 0 (* already registered *) else
    get groupkey_table(=encryptedFor2, =encryptedBy, k2:bitstring, =groupKeyID) in 0 (* already registered *) else
    insert groupkey_table(encryptedFor1, encryptedBy, groupKeyEncrypted1, groupKeyID);
    insert groupkey_table(encryptedFor2, encryptedBy, groupKeyEncrypted2, groupKeyID);
    out(c, TEPENC(sessionKey, (ResponseGroupKeyID, groupKeyID, nonce)))
  ).

  let MessagingServer_query(msg:bitstring, sessionKey:TEPSessionKey) =
    let decrypted: bitstring = TEPDEC(sessionKey, msg) in
    let (=QueryPublicKey, id:ID, nonce:coins) = decrypted in
    (
      get publickey_table(=id, pubKey:G) in
      out(c, TEPENC(sessionKey, (ResponsePublicKey, id, pubKey, nonce)))
    )
    else let (=QueryGroupKey, groupKeyID:ID, encryptedFor:ID, nonce:coins) = decrypted in
    (
      get groupkey_table(=encryptedFor, encryptedBy:ID, groupKeyEncrypted:bitstring, =groupKeyID) in
      out(c, TEPENC(sessionKey, (ResponseGroupKey, encryptedFor, encryptedBy, groupKeyEncrypted, groupKeyID, nonce)))
    ).

  let MessagingServer() =
    !(
      in(c, msg:bitstring);
      (
        MessagingServer_register(msg, Client1TEPSessionKey) |
        MessagingServer_register(msg, Client2TEPSessionKey) |
        MessagingServer_register(msg, Client3TEPSessionKey) |
        (* MessagingServer_register(msg, AttackerTEPSessionKey) | *)
        MessagingServer_query(msg, Client1TEPSessionKey) |
        MessagingServer_query(msg, Client2TEPSessionKey) |
        MessagingServer_query(msg, Client3TEPSessionKey) |
        MessagingServer_query(msg, AttackerTEPSessionKey)
      )
    ).

コマンドが RegisterPublicKey の場合，受け渡された公開鍵をテーブル publickey_table に登録， コマンドが RegisterGroupKey2 の場合，受け渡された暗号化されたグループ共通鍵をテーブル groupkey_table に登録します．

また，コマンドが QueryPublicKey の場合，受け渡されたユーザー ID に対応する公開鍵を publickey_table から取り出して返し，コマンドが QueryGroupKey の場合，受け渡されたグループID, ユーザーIDに対応する暗号化されたグループ共通鍵を publickey_table から取り出し返します．

攻撃者は，公開鍵やグループ共通鍵をメッセージングサーバへ登録することはできませんが，取得することはできます．

Client1の定義

Client1 は，グループのメンバの一人(Member A)に対応し，グループを作成し，Client2 (Member B)から送信されるグループメッセージを受信して復号する役割を担当します．

具体的には，「ホワイトペーパーの説明からシーケンス図を作成」節の，

  • 1. ユーザの鍵ペアの作成，公開鍵の登録
  • 2. グループ共通鍵の作成・登録
  • 5. グループメッセージを受信

に対応する処理を行います．ProVerif のモデルは，これらの処理を自然に ProVerif のサブプロセスとして定義しています:

(* Client1 subprocess *)
let Client1(c1id:ID, c2id:ID, c3id:ID) =
  (* register public key *)
  new c1cpr:scalar;
  let c1cpu = sca(c1cpr, Ggen(J)) in
  new n0: coins;
  out(c, TEPENC(Client1TEPSessionKey, (RegisterPublicKey, c1id, c1cpu, n0)));
  in(c, msg0:bitstring);
  let (=ResponseRegisterPublicKey, =c1id, =n0) = TEPDEC(Client1TEPSessionKey, msg0) in
  out(c, c1id);

  (* compute group shared key *)
  new sharedKey_gr:scalar;
  (* let sharedKey_gr_pu:G = sca(SharedKey_gr, Ggen(J)) in -- unused -- *)

  (* get public key of c2 *)
  new n1: coins;
  out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, c2id, n1)));
  in(c, msg1:bitstring);
  let (=ResponsePublicKey, =c2id, c2cpu:G, =n1) = TEPDEC(Client1TEPSessionKey, msg1) in

  (* get public key of c3 *)
  new n2:coins;
  out(c, TEPENC(Client1TEPSessionKey, (QueryPublicKey, c3id, n2)));
  in(c, msg2:bitstring);
  let (=ResponsePublicKey, =c3id, c3cpu:G, =n2) = TEPDEC(Client1TEPSessionKey, msg2) in

  (* register group shared key *)
  let key12:G = sca(c1cpr, c2cpu) in
  let key13:G = sca(c1cpr, c3cpu) in
  let sharedKey_gr_en12:bitstring = ENC(sharedKey_gr, key12) in
  let sharedKey_gr_en13:bitstring = ENC(sharedKey_gr, key13) in
  new groupKeyID: ID;
  new n3:coins;
  out(c, TEPENC(Client1TEPSessionKey, (RegisterGroupKey2, groupKeyID, c1id, (c2id, sharedKey_gr_en12), (c3id, sharedKey_gr_en13), n3)));
  in(c, msg3:bitstring);
  let (=ResponseGroupKeyID, =groupKeyID, =n3) = TEPDEC(Client1TEPSessionKey, msg3) in

  (* share groupKeyID *)
  out(c_pr, groupKeyID);

  !(
    (* receive group message (from c2) *)
  in(c, (=ver, =contentType, salt:coins, C:bitstring, mac:bitstring, senderID:ID, groupKeyID':ID));
  if (groupKeyID = groupKeyID') then
  (
    (* get public key of user who send message *)
    new n4: coins;
    out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, senderID, n4)));
    in(c, msg4:bitstring);
    let (=ResponsePublicKey, =senderID, cycpu:G, =n4) = TEPDEC(Client3TEPSessionKey, msg4) in

    let sharedSecret_gr = sca(sharedKey_gr, cycpu) in

    (* decrypt message *)
    let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in
    let MACp:bitstring = Hash(C) in
    let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in
    if (mac = MACe) then
    (
      let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in
      let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in
      let M':bitstring = sdeccbc(C, Ken, IVen) in
      event Client1_term1(Ken, IVen, senderID, groupKeyID)
    )
  )
  else
  (
    ...
  )
).

ProVerif スクリプトの (* register public key *) の部分で，鍵ペアを生成し，公開鍵 (c1cpu) を MessagingServer に登録し，

(* compute group shared key *) から (* share groupKeyID *) の部分で，グループ共通鍵 sharedKey_gr を生成し，グループの他のメンバーとの共通鍵を計算して (それぞれkey12, key13) ，それを利用してグループ共通鍵を暗号化し(それぞれsharedKey_gr_en12, sharedKey_gr_en13) ，グループID (groupKeyID) と共に，MessagingServer に登録し，プライベートチャネルc_pr を通してグループIDを他のメンバーに共有しています．

その後，(* receive group message (from c2) *) の部分で，Client2 が送信したメッセージを受信し，送信者の公開鍵とグループ共通鍵からグループ共通シークレット (sharedSecret_gr) を計算し，それを利用して，暗号化されたメッセージ (C)からMAC(MACe)を計算し，受信したメッセージに含まれるMAC(mac)との一致を確認し，暗号化されたメッセージを復号し平文 (M') を得ます．

Client2の定義

Client2 は，グループのメンバの一人(Member B) に対応し，グループメッセージを送信する役割を担当します．

具体的には，「ホワイトペーパーの説明からシーケンス図を作成」節の，

  • 1. ユーザの鍵ペアの作成，公開鍵の登録
  • 3. グループ共通鍵を取得
  • 4. グループメッセージを送信

に対応する処理を行います．ProVerif のモデルは，これらの処理を自然に ProVerif のサブプロセスとして定義しています:

(* Client2 subprocess *)
let Client2(c1id:ID, c2id:ID, c3id:ID) =
  (* register public key *)
  new c2cpr:scalar;
  let c2cpu = sca(c2cpr, Ggen(J)) in
  new n0: coins;
  out(c, TEPENC(Client2TEPSessionKey, (RegisterPublicKey, c2id, c2cpu, n0)));
  in(c, msg0:bitstring);
  let (=ResponseRegisterPublicKey, =c2id, =n0) = TEPDEC(Client2TEPSessionKey, msg0) in
  out(c, c2id);

  (* share groupKeyID *)
  in(c_pr, groupKeyID:ID);

  (* get encrypted groupKey *)
  new n1:coins;
  out(c, TEPENC(Client2TEPSessionKey, (QueryGroupKey, groupKeyID, c2id, n1)));
  in(c, msg1:bitstring);
  let (=ResponseGroupKey, =c2id, encryptedBy:ID, sharedKey_gr_en:bitstring, =groupKeyID, =n1) = TEPDEC(Client2TEPSessionKey, msg1) in

  (* get public key of user who encrypt groupKey *)
  new n2:coins;
  out(c, TEPENC(Client2TEPSessionKey, (QueryPublicKey, encryptedBy, n2)));
  in(c, msg2:bitstring);
  let (=ResponsePublicKey, =encryptedBy, cxcpu:G, =n2) = TEPDEC(Client2TEPSessionKey, msg2) in

  (* compute group key *)
  let key2x:G = sca(c2cpr, cxcpu) in
  let sharedKey_gr:scalar = DEC(sharedKey_gr_en, key2x) in
  !(
    (* encrypt message *)
    let sharedSecret_gr = sca(sharedKey_gr, c2cpu) in

    new salt:coins;
    let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in
    let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in
    let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in
    let C:bitstring = senccbc(M, Ken, IVen) in
    let MACp:bitstring = Hash(C) in
    let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in
    (* send group message *)
    event Client2_accept(Ken, IVen, c2id, groupKeyID);
    out(c, (ver, contentType, salt, C, MACe, c2id, groupKeyID))
  ).

ProVerif スクリプトの (* register public key *) の部分で，鍵ペアを生成し，公開鍵 (c2cpu) を MessagingServer に登録し，

(* share groupKeyID *) の部分で，プライベートチャネル c_pr を通して Client1 からグループIDを受け取り， (* get encrypted groupKey *) から (* compute group key *) の部分で，MessagingServer から暗号化されたグループ共通鍵を取得し，復号化してグループ共通鍵 (sharedKey_gr) を得て，

(* encrypt message *) から (* send group message *) の部分で，グループ共通シークレット (sharedSecret_gr) を計算し，それを利用して送信したい平文メッセージ (M) を暗号化し(C)，それを含むメッセージをチャネルcを通して送信します．

Client3の定義

Client3 は，グループのメンバの一人 (Member C) に対応し，Client2 (Member B)から送信されるグループメッセージを受信する役割を担当します．

具体的には，「ホワイトペーパーの説明からシーケンス図を作成」節の，

  • 1. ユーザの鍵ペアの作成，公開鍵の登録
  • 3. グループ共通鍵を取得
  • 5. グループメッセージを受信

に対応する処理を行います．ProVerif のモデルは，これらの処理を自然に ProVerif のサブプロセスとして定義しています:

(* Client3 subprocess *)
let Client3(c3id:ID) =
  (* register public key *)
  new c3cpr:scalar;
  let c3cpu = sca(c3cpr, Ggen(J)) in
  new n0: coins;
  out(c, TEPENC(Client3TEPSessionKey, (RegisterPublicKey, c3id, c3cpu, n0)));
  in(c, msg0:bitstring);
  let (=ResponseRegisterPublicKey, =c3id, =n0) = TEPDEC(Client3TEPSessionKey, msg0) in
  out(c, c3id);

  (* share groupKeyID *)
  in(c_pr, groupKeyID:ID);
  !(
    (* receive encrypted group message (from c2) *)
    in(c, (=ver, =contentType, salt:coins, C:bitstring, mac:bitstring, senderID:ID, =groupKeyID));
    new n1:coins;
    out(c, TEPENC(Client3TEPSessionKey, (QueryGroupKey, groupKeyID, c3id, n1)));
    in(c, msg1:bitstring);
    let (=ResponseGroupKey, =c3id, encryptedBy:ID, sharedKey_gr_en:bitstring, =groupKeyID, =n1) = TEPDEC(Client3TEPSessionKey, msg1) in

    (* get public key of user who encrypt groupKey *)
    new n2:coins;
    out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, encryptedBy, n2)));
    in(c, msg2:bitstring);
    let (=ResponsePublicKey, =encryptedBy, cxcpu:G, =n2) = TEPDEC(Client3TEPSessionKey, msg2) in

    (* compute group key *)
    let key3x:G = sca(c3cpr, cxcpu) in
    let sharedKey_gr:scalar = DEC(sharedKey_gr_en, key3x) in

    (* get public key of user who send message *)
    new n3: coins;
    out(c, TEPENC(Client3TEPSessionKey, (QueryPublicKey, senderID, n3)));
    in(c, msg3:bitstring);
    let (=ResponsePublicKey, =senderID, cycpu:G, =n3) = TEPDEC(Client3TEPSessionKey, msg3) in

    let sharedSecret_gr = sca(sharedKey_gr, cycpu) in

    (* decrypt message *)
    let Ken:key = ToKey(Hash((sharedSecret_gr, salt, Key))) in
    let MACp:bitstring = Hash(C) in
    let MACe:bitstring = sencecb(xor(breakf(MACp), breakb(MACp)), Ken) in
    if (mac = MACe) then
    (
      let IVpre:bitstring = Hash((sharedSecret_gr, salt, IV)) in
      let IVen:iv = ToIV(xor(breakf(IVpre), breakb(IVpre))) in
      let M':bitstring = sdeccbc(C, Ken, IVen) in
      event Client3_term(Ken, IVen, senderID, groupKeyID)
    )
  ).

ProVerif スクリプトの (* register public key *) の部分で，鍵ペアを生成し，公開鍵 (c3cpu) を MessagingServer に登録し，

(* share groupKeyID *) の部分で，プライベートチャネルc_pr を通して Client1 からグループIDを受け取り， (* receive group message (from c2) *) の部分で，Client2が送信したメッセージを受信し， (* get encrypted groupKey *) から (* compute group key *) の部分で，MessagingServer から暗号化されたグループ共通鍵を取得し，復号化してグループ共通鍵 (sharedKey_gr) を得て，

(* get public key of user who send message *) の部分で，送信者の公開鍵とグループ共通鍵からグループ共通シークレット (sharedSecret_gr) を計算し， (* decrypt message *) の部分で，グループ共通シークレットを利用し，暗号化されたメッセージ (C)からMAC(MACe)を計算し，受信したメッセージに含まれるMAC(mac)との一致を確認し，暗号化されたメッセージを復号し平文 (M') を得ます．

Main processの定義

Main Process では，Client1 … Client3 と MessagingServer を並列に実行させています:

(* Main process *)
process
new c1id:ID; new c2id:ID; new c3id:ID;
(
  Client1(c1id, c2id, c3id) |
  Client2(c1id, c2id, c3id) |
  Client3(            c3id) |
  MessagingServer()
)

クエリーとイベントの定義

作成した ProVerif のモデルに対し，以下の性質を検証するためのクエリーを定義しています:

  • メッセージの秘匿性

    Client2 が送信し，Client1 と Client3 が受け取るメッセージの内容を，攻撃者が把握できない

  • 認証性(injective):

    • Client3 が受信したメッセージを正常に復号し，メッセージを取得できた場合，そのメッセージは Client2 が送信している

    • かつ，送信回数 >= 受信したメッセージを正常に復号してメッセージを取得できた回数 (リプレイ攻撃無し)

    (Client1 が受信の場合も同様)

  • 認証性(non-injective):
    • Client3 が受信したメッセージを正常に復号し，メッセージを取得できた場合，そのメッセージは Client2 が送信している

    (Client1 が受信の場合も同様)

Client1, Client3 が，受信したメッセージを正常に復号してメッセージを取得できた時点と，Client2 がメッセージを送信する時点を指定するために，イベント Client3_term, Client1_term, および Client2_accept を使用します:

(* Verification of Secrecy and Authenticity *)
(* Secrecy of message *)
query attacker(M).

(* Events *)
event Client1_term1(key, iv, ID, ID).  (* msesageSenderID, message, senderID, groupKeyID *)
event Client1_term2(key, iv, ID, ID).  (* msesageSenderID, message, senderID, groupKeyID *)
event Client2_accept(key, iv, ID, ID). (* msesageSenderID, message, senderID, groupKeyID *)
event Client3_term(key, iv, ID, ID).   (* msesageSenderID, message, senderID, groupKeyID *)

...

(* Authenticity *)
query k:key, v:iv, senderID:ID, groupKeyID:ID; inj-event(Client3_term(k, v, senderID, groupKeyID)) ==> inj-event(Client2_accept(k, v, senderID, groupKeyID)).
query k:key, v:iv, senderID:ID, groupKeyID:ID; inj-event(Client1_term1(k, v, senderID, groupKeyID)) ==> inj-event(Client2_accept(k, v, senderID, groupKeyID)).

(* Secrecy of message *)の部分がメッセージの秘匿性を確認するためのクエリー， (* Authenticity *)の部分が認証性を確認するためのクエリーです． この認証性を確認するためのクエリーでは，まず認証性(injective)の検証が行われ，結果が成立とならなかった場合は認証性(non-injective)の検証が行われます．

(* Events *)の部分がイベントの定義です． ここで定義されるイベントは，Client1, … Client3 サブプロセスの中で使われていますので，それぞれのサブプロセスの定義を参照してください．

ProVerif のモデルの検証

[2] の E2EEP-1:N プロトコルの説明を元にシーケンス図を作成し，それを元に作成した ProVerif モデルを proverif コマンドで検証します．

検証時の操作ログを以下に示します． 実際のログは長いため，あまり重要ではない部分を省略し ... としました．

$ ls
LINE_E2EEP1n.pv
$ proverif --help
Proverif 2.00. Cryptographic protocol verifier, by Bruno Blanchet, Vincent Cheval, and Marc Sylvestre
...
$ time proverif LINE_E2EEP1n.pv
...
-- Query not attacker(M[])
...
RESULT not attacker(M[]) is true.
-- Query inj-event(Client3_term(k_366,v_367,senderID_368,groupKeyID_369)) ==> inj-event(Client2_accept(k_366,v_367,senderID_368,groupKeyID_369))
...
Could not find a trace corresponding to this derivation.
RESULT inj-event(Client3_term(k_366,v_367,senderID_368,groupKeyID_369)) ==> inj-event(Client2_accept(k_366,v_367,senderID_368,groupKeyID_369)) cannot be proved.
RESULT (but event(Client3_term(k_40469,v_40470,senderID_40471,groupKeyID_40472)) ==> event(Client2_accept(k_40469,v_40470,senderID_40471,groupKeyID_40472)) is true.)
-- Query inj-event(Client1_term1(k_370,v_371,senderID_372,groupKeyID_373)) ==> inj-event(Client2_accept(k_370,v_371,senderID_372,groupKeyID_373))
...
Could not find a trace corresponding to this derivation.
RESULT inj-event(Client1_term1(k_370,v_371,senderID_372,groupKeyID_373)) ==> inj-event(Client2_accept(k_370,v_371,senderID_372,groupKeyID_373)) cannot be proved.
RESULT (but event(Client1_term1(k_75039,v_75040,senderID_75041,groupKeyID_75042)) ==> event(Client2_accept(k_75039,v_75040,senderID_75041,groupKeyID_75042)) is true.)

real    0m4.494s
user    0m4.187s
sys     0m0.110s

$

検証結果は以下のようになりました:

  • メッセージの秘匿性: 成立
  • 認証性(injective): Client2–Client1 間と Client2–Client3 間のいずれも不成立
  • 認証性(non-injective): Client2–Client1 間と Client2–Client3 間のいずれも成立

認証性(injective)の検証結果が不成立となった原因について，ProVerif が出力するトレースを調べてみると，Client2 が Client1 または Client3 へ送信するメッセージを攻撃者がコピーして送信していました． このことから，E2EEP-1:N プロトコルの ProVerif のモデルはリプレイ攻撃に対して脆弱であることがわかりました．

今回は，攻撃者の能力に制限を与えたモデルで検証を行いましたが，この制限を取り除いたモデルに対して検証をすれば，今回は検出できなかった脆弱性を発見できるかもしれません． しかし，今回の挑戦はここまでとします． お疲れ様でした．

まとめ

以下の作業を行いました:

  1. 論文 [1] を読む
  2. Line の ホワイトペーパー [2] を読み E2EEP-1:N プロトコルを理解し，それを元にシーケンス図を作成
  3. シーケンス図を元に ProVerif のモデルを作成
  4. 作成した ProVerif のモデルを検証
    • 検証内容: メッセージの秘匿性, 認証性(injective), 認証性(non-injective)

ProVerif のモデルの検証から，以下の結果を得ました:

  • メッセージの秘匿性: 成立
  • 認証性(injective): 不成立 (ProVerifのモデルはリプレイ攻撃に対して脆弱)
  • 認証性(non-injective): 成立

注意

概要でも述べましたが， 今回の検証結果は，[2] で説明されている内容のみに基づき作成した ProVerif のモデル上で成立するものであり，実際に利用されているプロトコルでも同様に成立かどうかは不明であることに注意してください． 以下の理由から，今回の Proverif のモデルに対する検証結果が実際のプロトコルでも同様に成立する可能性は低いと思われます:

  • [2] は，プロトコルの概要を説明するのに十分な程度の抽象度となっていて，実際に動作するプログラムを作成できるほど詳細なものではありません
  • [2] が実際に使われているプロトコルを正確に説明しているとは限りません
    • 実際には様々な安全確保のための技術が組み込まれていることが予想されます
  • 今回作成した ProVerif のモデルは，[2] の E2EEP-1:N プロトコルの説明と一部異なる部分があります
  • 今回作成した ProVerif のモデルに誤りがあるかもしれません

謝辞

このブログの公開にあたり，LINE株式会社様および茨城大学の米山一樹先生に事前に内容を確認して頂きました．深く感謝申し上げます．

References