同型暗号の「ノイズで隠す」を機械が検証する — 適応的な問い合わせに強い安全性証明
📄 Verified Pythagorean Composition for Adaptive Cryptographic Games: Noise Flooding in Homomorphic Encryption
✍️ Lee, Y., Cojocaru, A., Liu, J., Wu, X.
📅 論文公開: 2026年8月
3つのポイント
- 1
暗号化したまま計算できる「近似同型暗号」では、計算結果に含まれる誤差から中身が漏れないよう、あえて大きなノイズを足して隠す（ノイズフラッディング）という定番の防御があります。
- 2
この防御は、攻撃者が何度も繰り返し問い合わせる状況で安全性の余裕が急速に目減りしてしまうのが弱点でしたが、本研究は目減りを問い合わせ回数の平方根の程度に抑える証明を与えました。
- 3
しかもその証明を人手のレビューだけに委ねず、証明支援系 Rocq と暗号証明フレームワーク SSProve の上で機械検証（マシンチェック）した点が本研究の中心的な貢献です。
論文プロフィール
- 著者: Yi Lee, Alexandru Cojocaru, Junyi Liu, Xiaodi Wu
- 発表年 / 掲載先: 2026 年、arXiv（cs.CR: 暗号とセキュリティ）
- 研究対象: 近似同型暗号（データを暗号化したまま計算できる方式のうち、結果に誤差が残るタイプ）における「ノイズフラッディング」という防御手法の安全性証明
- 研究内容: 攻撃者が復号結果を何度も問い合わせる「適応的」な状況で、従来の証明手法だと安全性の余裕が問い合わせ回数に比例して失われていました。本研究は条件付き KL コストという量を積み上げてから最後に一度だけ統計的距離へ変換する方針をとり、失われる量を平方根の程度に抑えます。さらにその議論全体を証明支援系の上で機械検証しています。
エディターズ・ノート
「暗号化したまま扱う」という約束は、実装が正しいだけでは足りず、その安全性の論証そのものが正しくなければ成立しません。この論文は、プライバシー技術の信頼を「人間のレビューを通った紙の証明」から「機械が検証した証明」へ一段引き上げようとする試みで、私たちが家族の記録を預かるうえで最も学びたい姿勢が詰まっています。
実験デザイン
本研究は実測実験ではなく、定理を証明し、その証明を機械に検証させるタイプの研究です。
- 対象とする設定: 近似的に正しく（approximately correct）、かつ IND-CPA 安全な同型暗号方式が与えられたとき、そこにノイズフラッディングを施した方式が IND-CPAD という、より強い攻撃モデルでどれだけ安全かを問います。
- IND-CPAD とは: 攻撃者が暗号文だけでなく復号結果も繰り返し受け取れるという、より現実に近い攻撃モデルです。ここでの問い合わせ回数を q と呼びます。
- 示された上界: ノイズフラッディング版の攻撃成功確率は、元の方式に対する IND-CPA での優位性に、√(qn) を 2γ で割った項を足した値以下に抑えられます。ここで n は平文の次元、γ はノイズの幅を何倍に広げるかを表す係数です。
- 要点: 誤差項が q に比例するのではなく √q に比例することが、実際に使える鍵長・ノイズ幅を決めるうえで決定的に効きます。
| 系列 | 適応的な問い合わせ回数 q | 失われる安全性の余裕（相対値） |
|---|---|---|
| 従来の合成（qに比例） | 1 | 1 |
| 従来の合成（qに比例） | 4 | 4 |
| 従来の合成（qに比例） | 16 | 16 |
| 従来の合成（qに比例） | 64 | 64 |
| 本研究（√qに比例） | 1 | 1 |
| 本研究（√qに比例） | 4 | 2 |
| 本研究（√qに比例） | 16 | 4 |
| 本研究（√qに比例） | 64 | 8 |
🔍 なぜ「一度だけ変換する」と得をするのか
従来の標準的な議論では、q 回の応答を 1 回ずつ「統計的に近いシミュレーション」で置き換え、それを順番につないでいきます（ハイブリッド論法）。このとき置き換え 1 回ごとに誤差が足し算されるため、合計は q に比例します。
本研究は、各ステップの近さを統計的距離ではなく条件付き KL ダイバージェンスというコストとして保持したまま積み上げ、最後に一度だけ統計的距離へ換算します。KL から統計的距離への変換は平方根を伴うため（Pinsker の不等式の形）、q 個のコストを足してから平方根を取る形になり、√q の目減りで済むという構図です。
この「足してから最後に平方根」という構造を、著者らは SSProve の意味論の上に新しく作った関係的プログラム論理の Pythagorean judgment（ピタゴラス判定） として定式化しています。
🔍 この研究の限界と注意点
誠実にお伝えしたい点がいくつかあります。
- 上界であって最適性の主張ではありません: √q という評価は「これ以上悪くはならない」という保証であり、実際の攻撃がこの限界まで到達することを示したものではありません。
- 前提条件つきの結果です: 元の同型暗号方式が近似的に正しく IND-CPA 安全であること、という仮定の上に成り立つ相対的な安全性です。
- 形式検証の範囲: 機械検証されているのは論文が形式化した還元（リダクション）とその評価であり、実装されたライブラリのコードが安全であることまでを直接保証するものではありません。
技術的背景
同型暗号は、データを暗号化したまま計算できる技術です。サーバー側は中身を見ないまま処理でき、結果を受け取った持ち主だけが復号できます。 エンドツーエンド暗号化 エンドツーエンド暗号化 送信者と受信者の間でデータを暗号化し、途中のサーバーでも内容を復号できないようにする暗号化方式。 が「運ぶあいだ隠す」技術だとすれば、同型暗号は「計算しているあいだも隠す」技術だと言えます。
ただし近似同型暗号では、復号した結果にわずかな計算誤差が残ります。この誤差のかたちが、元のデータや秘密鍵の手がかりになってしまう——これが復号結果を悪用する攻撃の入り口でした。対策がノイズフラッディング、つまり「本物の誤差が埋もれるくらい大きなノイズを、わざと足してから返す」という発想です。砂粒の位置を隠すために、砂場ごと均してしまうようなイメージです。
この「ノイズで隠す」という発想は、 差分プライバシー 差分プライバシー データにノイズを加えることで、個人のデータが含まれているかどうかを統計的に区別できなくする数学的プライバシー保証。 と同じ系譜にあります。差分プライバシーでも、統計値にノイズを足して個人の寄与を見えなくします。そして両者に共通する最大の悩みが、問い合わせを繰り返されたときの安全性の目減り（合成）です。本研究が扱う条件付き KL コストの積み上げは、差分プライバシーの分野で発展してきた高度な合成定理の考え方と響き合うものです。
🔍 Rocq と SSProve という道具立て
- Rocq: 定理証明支援系です（かつて Coq と呼ばれていたものの現行名）。人間が書いた証明の一歩一歩を機械がチェックし、論理の飛躍を許しません。
- SSProve: 暗号の安全性証明を、ゲームベースの書き換えとして Rocq の上で扱うためのフレームワークです。攻撃者との「ゲーム」を少しずつ書き換えていく、暗号研究者にとって自然な証明スタイルをそのまま形式化できます。
著者らはさらに、局所的なオラクル規則を任意の適応的プログラムへ持ち上げる検証済みトレースコンパイラを作っています。「1 回の応答について成り立つ性質」を「何度問い合わせても成り立つ性質」へ、機械検証されたまま拡張する部品だと考えてください。
And Family Voice としての解釈
視点A（プロダクトの思想として）
And Family Voice は、音声を端末の外へ出さない オンデバイス推論 オンデバイス推論 クラウドにデータを送信せず、端末上でAIモデルの推論を完結させる技術。低遅延とプライバシー保護を両立する。 で文字起こしを行い、Human-in-the-Loop の承認フローを通ったテキストだけを E2EE でクラウドに預ける設計をとっています。この論文は同型暗号という別の技術領域の話ですが、私たちが受け取った示唆は技術の選択そのものではなく、保証の語り方にあります。
- 「一度きり」ではなく「繰り返し」を前提に考える: IND-CPAD が示すのは、現実の攻撃者は一回で諦めないという事実です。私たちも、暗号化されたデータへのアクセスや復号の機会が積み重なったときに何が起きるかを、単発のケースとは分けて見積もる必要があると考えています。
- 証明可能性を設計の評価軸に入れる: 「安全そうな実装」ではなく「なぜ安全と言えるかを書き下せる設計」を選ぶ。機械検証まで到達できるかは別として、私たちの E2EE（AES-256-GCM）まわりの設計判断も、根拠を文章として残せる形で積み上げていきたいと考えています。
- 匿名化やノイズ付与に安易に頼らない: 音声匿名化 音声匿名化 話者の個人情報（声紋・話者特性）を除去または変換しつつ、発話内容を保持する音声処理技術。 のような「加工して守る」手法を検討する際も、この論文が教えるとおり、繰り返し使われたときの目減りまで含めて評価すべきだと受け止めています。まだ私たちも探求の途中です。
視点B（読者の方が今日から意識できること）
「暗号化しています」という説明を見たとき、それは何から何を守る暗号なのかを一度だけ考えてみてください。通信経路だけを守るのか、預けた先のサーバー管理者からも守るのか、あるいは計算しているあいだも守るのか。守備範囲は方式ごとに大きく違います。サービスのプライバシーポリシーで「保存時に暗号化」と「エンドツーエンド暗号化」が使い分けられているかを見るだけでも、そのサービスがどこまで本気かが見えてきます。
読後感
私たちは、プライバシー保護の技術を語るとき、つい「安全です」という結論だけを差し出しがちです。けれどこの論文が丁寧に積み上げていたのは、結論ではなくその結論に至る道筋を、他人が——そして機械が——検証できる形にすることでした。
あなたが日々使っているサービスの「安全です」は、どこまで確かめられる形で語られているでしょうか。そして、私たちが家族の記録という代えのきかないものを預かる立場として、その問いにどこまで誠実に答えられるでしょうか。引き続き考え続けたいテーマです。