祝RFC！Transport Layer Security (TLS) 1.3 発行の軌跡 ～熟成された4年間の安全性解析～

こんにちは、エンジニアの米澤です。

2018年8月、Transport Layer Security (TLS) プロトコルの最新版である TLS 1.3 が RFC 8446 として発行されました。 TLS はインターネット上でセキュアな通信路を確立するためのプロトコルで、 現代のインターネットにおいて欠かせない技術のひとつです。 TLS 1.3 の仕様策定が開始されたのが2014年ですので、実に丸4年かかったことになります。ドラフトバージョンが実に28版 (draft 28) まで至ったことからも、 その長い道のりが伺えます。

TLS 1.3 にはさまざまな特徴がありますが、 中でも注目したいのが、セキュリティに関して「プロトコルの安全性が証明されている」と言われていることです。 TLS 1.2 以前と異なり、TLS 1.3 の仕様策定には最初から複数の暗号学者が参画し、さまざまな形で安全性証明を試み、実際の攻撃も発見されました。 また、暗号分野の権威ある国際会議である CRYPTO 2018 の併設ワークショップとして CWTLS 1.3 (Crypto Welcomes TLS 1.3) が開催されるなど、 TLS 1.3 は暗号学者からも大きな注目を浴びていることが分かります。

さて、ここで「安全性が証明されている」とはどういうことか、お分かりになるでしょうか？ さらに、「プロトコルの安全性」とは…？

本記事では、安全性とは何か、暗号理論における安全性の証明とは何かを説明し、TLS 1.3 が達成する安全性について暗号理論の視点で解説します。

なお、本記事では暗号理論における安全性について分かりやすく解説することを心がけておりますが、 一部暗号理論に関する知識を必要とする部分がございます。その場合は、解説の前にその旨記載しております。本記事により、皆様が少しだけでも「安全性」について理解を深められたらと願っています。

目次

• 安全とは？
  • 「安全性」の考え方
  • 証明可能安全性
  • 安全性の証明手法
    • 暗号解析
    • 形式検証
    • Verifiable Implementation
  • まとめ
• TLS 1.3 について
  • 特徴
  • 安全性要件
    • ハンドシェイクプロトコルの安全性要件
    • レコードプロトコルの安全性要件
  • まとめ
• TLS 1.3 の安全性証明
  • 実際に見つかった攻撃
    • ダウングレード攻撃
    • セッション再開への攻撃
    • 0-RTT への攻撃
  • 証明された安全性
  • まとめ
• おわりに

安全とは？

「安全性」の考え方

皆様がインターネット上で何らかのITサービスを利用するとき、 「このサービスのセキュリティはバッチリです！安全です！」と言われたら、 一体どんな状態だと思われるでしょうか？ 個人情報が漏れない？不正アクセスされない？

一般的に、システムやサービスが「安全である」とは、ある能力を持つ攻撃者に対して、ある安全性の性質（「安全性要件」や「セキュリティ要件」と呼びます）が達成される状態のことを言います。

例えば、攻撃者としてよく知られているのが中間者 (Man In The Middle: MITM) です。 中間者は、通信を行う2者間に割り込み、通信の内容を盗聴したり改ざんしたりします。 安全性要件の例としてよく知られているのが、他人に情報を知られないようにする「機密性 (Confidentiality)」、情報が改ざんされないようにする「完全性 (Integrity)」、継続して使用できるようにする「可用性 (Availability)」で、「情報セキュリティのCIA」などと呼ばれています。 実際の安全性要件では、CIA をそれぞれ詳細化したものが採用されます。例えば機密性に対しては、「攻撃者にメッセージの全部が知られない」「攻撃者にメッセージの一部が知られない」などのバリエーションが考えられます。

証明可能安全性

それでは、システムやサービスが「安全である」ことを示すにはどうすればいいのでしょうか。これ以降、システムやサービスの機能を実現するための手段のことを「プロトコル」と呼ぶことにします。

プロトコルが「安全である」ことを示すとき、まずはプロトコルで想定する攻撃者を厳密に定義（モデル化）します。次に、プロトコルが達成すべき安全性要件を記述します。「プロトコル」が「想定される攻撃者」に対して「安全性要件」を満たすとき、プロトコルは「安全である」と言えます。

このとき、「安全性要件を満たす」ことを何らかの証明手法を用いて理論的に証明することができるとき、プロトコルは 証明可能安全性 (provable security) を有する 、または 証明可能安全 (provably secure) である と言います。

安全性の証明手法

プロトコルの安全性を証明するための手法には、暗号解析と形式検証の2種類があります。

暗号解析

暗号理論で広く使われる証明手法（暗号解析と呼ぶことにします）について説明します。 ここでは特に、計算量的安全性と呼ばれる安全性に対する証明手法について解説します。

暗号解析、特に計算量的安全性の証明では、攻撃者を定義する際、 計算量モデル (computational model) と呼ばれる攻撃モデルを使います。 ここで「計算量」とは、コンピュータ等でプログラムを実行するのにかかる時間やステップ数だと捉えてください。

計算量モデルでは、攻撃者は現在一般的に使用されているコンピュータ（専門用語で確率的チューリングマシンと呼びます）と仮定され、プロトコルの構成要素となる暗号プリミティブはビット列からビット列への関数として表されます。つまり、攻撃者は暗号プリミティブへの入力を自由に変更し、好きな出力を取得することができます。また、セキュリティパラメータと呼ばれる値を導入し、攻撃者の計算量はセキュリティパラメータの関数として評価されます。この攻撃モデルを基本として、具体的な攻撃方法を攻撃者の能力として定式化します。

安全性要件は、その安全性要件が満たされない確率がセキュリティパラメータに対して無視できる確率であるとき、安全であるとされます。

暗号解析における（計算量的）安全性証明では、以下の事実を数学的に証明します。

攻撃者の能力を仮定したとき、プロトコルの安全性要件を破ることは、数学的に難しいと知られている問題を解くことに帰着される。

つまり、計算量的安全性とは、「現在考えうる高性能なコンピュータを使って計算しても、プロトコルの安全性要件を破ることはできない」ことを意味します（ちなみに、攻撃者として量子コンピュータを仮定する暗号系も現在研究されていますが、それはまた別の話）

計算量的安全性では、プロトコルの安全性要件を破るためのコストが計算量として示されるため、より定量的に安全性を評価することができます。

暗号解析は一般的に、攻撃者の能力と安全性要件を人力で考え、数学的帰着を手作業で証明します。 この証明には暗号理論に対する深い知識が必要となり、また複雑なプロトコルに対する証明は非常に難しく、簡単にできる作業ではありません。 また、計算量的安全性の証明の自動化は難しいとされていますが、CryptoVerif を始めとして暗号解析の一部を機械化するためのツールも開発されています。

TLS 1.3 の安全性証明では、人力による暗号解析とツールを用いた暗号解析の両方が用いられています。本記事では、前者を古典的暗号解析、後者を半自動暗号解析と呼ぶことにします。

形式検証

続いて、形式検証を用いたプロトコルの安全性証明手法について説明します。

形式検証では、攻撃者を定義する際、 記号モデル (symbolic model) と呼ばれる攻撃モデルを使います。 記号モデルでは、プロトコルを構成する暗号プリミティブはブラックボックスとして与えられます。つまり、計算量モデルでは暗号プリミティブの入力自体を操作できますが、記号モデルでは暗号プリミティブを通じた計算のみが許されています。

形式検証におけるプロトコルの安全性証明では、以下の事実を証明します。

攻撃者の能力を仮定したとき、プロトコルの安全性要件を破るような攻撃手順が発見されない。

ここで、形式検証では想定された攻撃者による攻撃の存在を発見することはできるが、必ずしも攻撃が存在しないことの証明とはならないことに注意しましょう。これは、現実的な計算時間で攻撃を発見するために、形式検証ツールではしばしば攻撃空間に制限を加えることによります。

プロトコルの形式検証は自動化に適しているため、さまざまな自動形式検証ツールが開発されています。代表的な自動形式検証ツールとして、ProVerif や Tamarin が挙げられます。

計算量モデルと記号モデルで証明できる安全性の差についてはさまざまな研究が行われています。記号モデルにおける攻撃はそのまま計算量モデルにおける攻撃となりますが、その逆は必ずしも成り立たないことが知られています。すなわち、記号モデルにおいて安全なプロトコルでも、計算量モデルにおいて攻撃が存在する場合があります。

Verifiable Implementation

ここで、厳密には証明手法ではないですが、安全なプロトコルを実装する上で重要な技術を紹介します。

プロトコルの仕様がいくら安全だからといって、実装に不具合があったら、そのプロトコルおよびそれを用いたシステムやサービスは安全とは言えません。そこで、実装されたコードの安全性を検証する技術 (verifiable implementation) が提案されました。

検証可能実装には2種類のアプローチが存在します。 ひとつは、モデル記述言語で記述された仕様を、正しいと証明されている適切なコンパイラを使用して実装に翻訳するアプローチです。 もうひとつは、実装されたコードそのものを解析するアプローチです。 実装そのものを解析する場合、実装から ProVerif 等の形式検証ツールの入力となるようなプロトコル仕様を抽出する方法が考えられます。

TLS 1.3 に対しては、F* と呼ばれるプログラム検証に適した関数型プログラミング言語を用いた verifiable implementation が報告されています。

まとめ

• 「安全である」とは、ある能力を持つ攻撃者に対し、ある安全性の性質（安全性要件）が達成される状態のこと
• プロトコルが安全性要件を満たすことが理論的に証明されるとき、プロトコルは証明可能安全性を有する
• 安全性の証明手法には「暗号解析」と「形式検証」が存在し、攻撃者の定義に「暗号解析」では計算量モデルが、「形式検証」では記号モデルが適用される

TLS 1.3 について

続いて、本記事のテーマである TLS 1.3 について説明します。

特徴

TLS 1.3 の詳細については、 wolfSSLの紹介ページ や 山本和彦さんの解説資料(PDF) や 大津繁樹さんの講演資料(PDF) 等、 非常に充実した解説がインターネットで公開されておりますので、 そちらをご参照いただくのが良いかと思います （ただしこれらはTLS1.3のドラフト版を基にした説明であることにご注意ください）。 ここでは、TLS 1.3 の特徴を簡単に紹介します。

TLS には大きく分けて2つのプロトコルから構成されます。 ハンドシェイクプロトコル (Handshake Protocol) では、サーバとクライアント間で鍵交換と相手認証を行います。 レコードプロトコル (Record Protocol) では、ハンドシェイクプロトコルで交換したセッション鍵を利用してサーバとクライアントが暗号通信を行います。

ハンドシェイクプロトコルには3つのモードが存在します。 これらのモードのうち 0-RTT (Round Trip Time) はハンドシェイクなしで（事前共有鍵を用いて）暗号化データを送信するモードで、 TLS 1.3 で初めて採用されました。

• フルハンドシェイク (Full Handshake) : 通常のハンドシェイク
• セッション再開 (Session Resumption) : 事前共有鍵を利用して以前のセッションを再開
• 0-RTT : 事前共有鍵を利用して、鍵交換時に暗号化データを一緒に送信

その他、TLS 1.2 以前と比較して、TLS 1.3 は以下の点が変更されています。

• フルハンドシェイクが 2-RTT から 1-RTT に変更された
• ハンドシェイクプロトコルのメッセージを暗号化できるようになった
• 暗号スイート (Cipher Suite: TLSで利用される暗号アルゴリズムの組み合わせ) の定義方法が変更された
• 暗号スイートの数が大幅に削減され、下位互換性のために残されていた安全でないアルゴリズムが軒並み削除された
• 鍵スケジュールが全面的に見直され、鍵導出に用いられる関数が HMACベースの擬似ランダム関数から HKDF (HMAC-based Extract-and-Expand Key Derivation Function) と呼ばれる鍵導出関数に変更された
• レコードプロトコルで使われる暗号アルゴリズムが認証暗号 (Authenticated Encryption with Associated Data: AEAD) のみとなった

安全性要件

前述の通り、TLS 1.3 では鍵交換・認証・（認証）暗号化が行われます。 それでは、TLS 1.3 は何をもって安全だと言われているのでしょうか？

フォーマルな定義ではありませんが、TLS 1.3 の RFC において、TLS 1.3 の達成する安全性要件として以下のような性質が挙げられています。攻撃者のどのような行動を制限しているのか、プロトコルが成立するためにどのような条件を掲げているのか、イメージが掴めるかと思います。

ハンドシェイクプロトコルの安全性要件

• 同一セッション鍵の確立：ハンドシェイクが正常終了したときには、サーバとクライアントで同一のセッション鍵が生成される。
• セッション鍵の秘匿性：共有されたセッション鍵は攻撃者に知られない
• 相互認証性（サーバ認証/クライアント認証）：クライアントはサーバを認証する。クライアント認証が行われる場合、サーバはクライアントを認証する。
• セッション鍵の一意性：2つの異なるセッションでは、関連性のない独立なセッション鍵が生成される。
• ダウングレード保護：暗号パラメータは両者の間で同一である。
• 長期鍵による前方秘匿性：ハンドシェイク後に長期鍵（証明書の署名鍵など）が漏洩しても、セッション鍵の安全性に影響はない。

レコードプロトコルの安全性要件

• 機密性：攻撃者はレコードプロトコルで送信されたデータを与えられても、平文を特定できない。
• 完全性：攻撃者はレコードプロトコルで送信されたデータと異なるデータを偽造できない。
• 順序保護性 / リプレイ不能性：攻撃者は受信者が既に受理したデータをもう一度受理させることはできない。または、N回のプロトコルにつきN+1回のデータを受理させることはできない。
• 鍵変更後の前方秘匿性：レコードプロトコルで用いる鍵が更新されたあとで攻撃者が送信者/受信者を乗っ取ったとしても、過去の鍵で暗号化されたデータを復号することはできない。

まとめ

• TLS は大きく分けて、鍵交換と相手認証を行う「ハンドシェイクプロトコル」と、データ暗号化を行う「レコードプロトコル」に分けられる
• 「ハンドシェイクプロトコル」は「フルハンドシェイク」「セッション再開」「0-RTT」の3種類のモードが存在する
• それぞれのプロトコルに対して安全性要件が挙げられている

TLS 1.3 の安全性証明

ここまでで、暗号理論における安全性とは何か、安全性をどのように証明するのか、TLS 1.3 が満たす安全性要件がどのようなものか、お分かりいただけたかと思います。

それではいよいよ、TLS 1.3 でどのような安全性が証明されたかを実際に見て行きましょう。 ここからの内容は、暗号理論に関する専門知識が必要となります。暗号理論的な解説にもう少し触れたいという方は、引き続きお付き合いください。

実際に見つかった攻撃

まずは、安全性証明の過程で実際に発見された攻撃を紹介します。 安全性証明は TLS 1.3 の仕様策定と並行して行われ、結果が随時報告されました。 攻撃に対する対策はフィードバックされ、 TLS 1.3 の仕様に反映されています。

ダウングレード攻撃

TLS 1.3 と TLS 1.2 以前とが混在するサーバにおいて、 TLS 1.2 以前のプロトコルの設定の影響で TLS 1.3 の安全性が破られる事例が発見されました。

Jagar らは、TLS 1.3 サーバが TLS 1.2 以前のバージョンで PKCS#1 v1.5 と呼ばれる static RSA 暗号化方式をサポートし、かつ TLS 1.3 と TLS 1.2 以前で同じサーバ証明書を使用している場合、攻撃者がサーバになりすますことができることを示しました。

Bhargavant らは、TLS 1.3 自体にダウングレード攻撃を防ぐ仕組みはあるものの、通信プロトコルを TLS 1.3 から TLS 1.2 以前にダウングレードさせることにより TLS 1.2 以前で知られているダウングレード攻撃が可能になることを示しました。

セッション再開への攻撃

Cremers らは、Tamarin を用いた形式検証により、draft 10 の事前共有鍵を用いたセッション再開におけるクライアント認証の脆弱性を発見しました。この脆弱性を利用して、中間者攻撃が可能な攻撃者がクライアントに成りすませることが判明しました。

この攻撃は、TLS 1.3 の仕様を検討する TLS WG で想定されておらず、 形式検証によって初めて発見されました。 この脆弱性は draft 11 で修正されました。

0-RTT への攻撃

TLS 1.3 の 0-RTT モードでは、事前共有鍵を用いた方法が採用されましたが、 draft 12 までは Diffie-Hellman (DH) 鍵共有を用いた方法も採用されていました。 しかし、DH 鍵共有を用いた方式では攻撃者による中間者攻撃が可能となることが分かりました。これにより、draft 13 以降では DH 鍵共有による 0-RTT モードは不採用となりました。

証明された安全性

それでは、TLS 1.3 で実際に証明された安全性を見て行きましょう。

ちなみに、 TLS 1.2 以前に対しても安全性を証明する試みは多くの研究者により実施されていました。 しかし、TLS 1.2 以前は暗号学者がプロトコル設計に関与していないこともあり、 数学的に難しい問題への帰着を示すのが難しく、 安全性を証明するのが非常に難しいプロトコルになっていました （暗号学者にとって非常に挑戦的な問題となっていたかもしれませんが…）

一方 TLS 1.3 では、暗号学者がプロトコル設計に関与することによって、 「安全性証明をつけやすい」プロトコルを設計することができたのです。

このような「証明しやすい」プロトコルに対し、暗号解析や形式検証による安全性証明が試みられました。

Dowling らは TLS 1.3 を暗号解析し、 フルハンドシェイクとセッション再開に対し2つの安全性要件を定義しました。

• Match security : 同じ情報で同じ手順を用いて通信したセッションのセッションIDは一致する
• Multi-Stage security: 攻撃者はハンドシェイクで導出されたセッション鍵と乱数列を区別できない

ちなみに、前章 ではいくつも安全性要件が挙げられているのに、2つしか安全性要件がないのはなぜ？と疑問に思われるかもしれませんが、いくつもの安全性要件がこれら2つの定義に集約されていると考えて頂ければ結構です（上記の安全性要件はかなりざっくりした説明で、実際にはさまざまな条件が定義されています）

また、TLS 1.3 の利用される場面（異なる暗号アルゴリズムによるハンドシェイクが並行に複数回実行される）に応じた攻撃モデルを定義しました。

そして、このように定義された攻撃モデルを仮定したとき、 TLS 1.3 (draft 10) が Match security と Multi-Stage security の両方を満たすことを証明しました。

また、Bhargavant らは ProVerif を用いて、以下の能力を持つ攻撃者を記述しました。

• 中間攻撃
• サーバまたはクライアントとの結託
• 弱い長期鍵の取得
• RSA 復号オラクル
• （ダウングレード攻撃による）弱い Diffie-Hellman 群の使用
• （ダウングレード攻撃による）弱いハッシュ関数の使用
• （ダウングレード攻撃による）弱い認証暗号の使用

このような攻撃者に対し、TLS 1.3 (draft 18) において以下の安全性要件を証明しました。

• 秘匿性
• 前方秘匿性
• 認証可能性
• リプレイ保護
• セッションIDの一意性

ちなみに、彼らの記述した ProVerif は、攻撃者の記述に400行、TLS 1.2 のプロセス記述に200行、TLS 1.3 のプロセス記述に 250行、TLS 1.2 の安全性要件記述に 50行、 TLS 1.3 の安全性要件記述に 180行を要し、検証はワークステーションを用いて70分かかったそうです。

TLS 1.3 の安全性証明を扱った主な論文を表に示します。 本記事では各論文の詳細は割愛させていただきますが、解説をご希望の方は別途ご連絡ください！

まとめ

• TLS 1.3の仕様策定中に安全性証明が行われ、実際に攻撃が発見された
• TLS 1.3 の暗号解析では、Match security と Multi-Stage security が証明された
• TLS 1.3 の形式検証では、ダウングレード攻撃を含む攻撃に対する安全性が証明された

おわりに

本記事では、TLS 1.3 がRFCとして発行されるまでの過程について、 安全性証明の観点から解説しました。 TLS 1.2 以前と異なり、仕様策定から暗号学者が関わったことにより、 TLS 1.3 は証明可能安全性を有するプロトコルとなりました。 運用開始後に多くの脆弱性が発見された過去の TLS と比較して、 プロトコルのセキュアデザインが成功した事例であると言えるでしょう。 TLS 1.3 の RFC が公開され、実際のシステムやサービスで適用が進むであろう今後、 TLS 1.3 の安全性に関する動向に注目です。

なお、 TLS 1.3 での成功事例を受けて、IETF の他の WG においても 仕様策定から安全性証明を試みる動きが見られます。 例えば Message Layer Security (MLS) WG では、 形式検証によりメッセージングプロトコルの安全性証明を実施しようとしています。

本記事で説明した通り、安全性証明にはさまざまな方法があり、証明できる安全性要件も異なります。 「サービスのセキュリティはバッチリです！」と言われるのを信じるだけではなく、プロトコルが何故安全なのか、システムやサービスのセキュリティは何故守られるのか、気にしてみてはいかがでしょうか。

なお、本記事では TLS 1.3 の理論的な側面を解説しましたが、 反響次第で（！）TLS 1.3 の実際の利用についても今後解説していけたらと考えております。