証明可能なセキュリティ

証明可能セキュリティとは、証明可能な あらゆるタイプまたはレベルのコンピュータ セキュリティを指します。さまざまな分野でさまざまな方法で使用されます。

通常、これは暗号学で一般的な数学的証明を指します。このような証明では、攻撃者の能力は敵対的モデル（攻撃者モデルとも呼ばれる）によって定義されます。証明の目的は、モデル化されたシステムのセキュリティを破るためには、攻撃者が根本的な困難な問題を解決しなければならないことを示すことです。このような証明では、サイドチャネル攻撃やその他の実装固有の攻撃は通常、システムを実装せずにモデル化することは不可能であるため、考慮されません（したがって、証明はこの実装にのみ適用されます）。

暗号化以外では、この用語はセキュア コーディングやセキュリティ バイ デザインと組み合わせて使用​​されることが多く、どちらも特定のアプローチのセキュリティを示すために証明に頼ることができます。暗号化の設定と同様に、これには攻撃者モデルとシステムのモデルが関係します。たとえば、モデルで記述された意図された機能とコードが一致することを検証できます。これは、静的チェックによって実行できます。これらの手法は、製品の評価に使用されることがあります ( Common Criteriaを参照)。ここでのセキュリティは、攻撃者モデルの正確さだけでなく、コードのモデルにも依存します。

最後に、証明可能セキュリティという用語は、ファイアウォール、ウイルス対策ソフトウェア、侵入検知システムなどのセキュリティ製品を販売しようとしているセキュリティ ソフトウェアの販売者によって使用されることがあります。これらの製品は通常、精査の対象ではないため、多くのセキュリティ研究者は、この種の主張をインチキ薬の販売であると考えています。

暗号学では、システムのセキュリティ要件が、敵対者がシステムにアクセスでき、十分な計算リソースも持っているという明確な仮定のもと、ヒューリスティックではなく敵対的モデルで形式的に述べられる場合、システムは証明可能なセキュリティを備えているとされます。セキュリティの証明 (「縮約」と呼ばれる) は、敵対者のシステムへのアクセスに関する仮定が満たされ、特定の計算タスクの困難さに関する明確に述べられた仮定が成り立つ場合に、これらのセキュリティ要件が満たされることです。このような要件と証明の初期の例として、ゴールドワッサーとミカリが、意味的セキュリティと、 2 次残余問題に基づく構築について示しました。セキュリティの証明の一部は、ランダム オラクル モデルなどの理論モデルに存在し、実際の暗号ハッシュ関数は理想化によって表されます。

証明可能なセキュリティに関する研究にはいくつかの流れがあります。1 つは、与えられた直感的に理解できるタスクに対するセキュリティの「正しい」定義を確立することです。もう 1 つは、一方向関数の存在など、可能な限り一般的な仮定に基づいた構成と証明を提案することです。大きな未解決の問題は、 P ≠ NPに基づいてそのような証明を確立することです。これは、 P ≠ NP の 予想から一方向関数の存在が導かれることは知られていないためです。

複数の研究者が、重要なプロトコルのセキュリティを主張するために使用された証明に数学的な誤りを発見しました。以下に示すそのような研究者の部分的なリストでは、研究者の名前の後に、まず証明とされる元の論文への参照、次に研究者が欠陥を報告した論文への参照が続きます。V. Shoup; ^{[1] [2]} AJ Menezes; ^{[3] [4]} A. Jha および M. Nandi; ^{[5] [6]} D. Galindo; ^{[7] [8]} T. Iwata、K. Ohashi、および K. Minematsu; ^{[9] [10]} M. Nandi; ^{[11] [12]} J.-S. Coron および D. Naccache; ^{[13] [14]} D. Chakraborty、V. Hernández-Jiménez、および P. Sarkar; ^{[15] [16]} P. Gaži および U. Maurer; ^{[17] [18]} SA Kakvi および E. キルツ。^{[19] [20]} および T. ホーレンシュタイン、R. キュンツラー、および S. テッサロ。^{[21] [22]}

コブリッツとメネゼスは、重要な暗号プロトコルの証明可能なセキュリティの結果は、証明に誤りが頻繁に含まれ、誤解を招くような解釈が多く、誤った保証を与え、通常、誤りであることが判明する可能性のある強力な仮定に依存し、非現実的なセキュリティ モデルに基づいており、研究者の注意を「旧式の」(数学的ではない) テストと分析の必要性からそらす役割を果たしていると書いています。これらの主張を裏付ける一連の論文^{[23] [24]}は、コミュニティで議論を呼んでいます。コブリッツとメネゼスの見解を否定した研究者の 1 人は、著名な理論家でFoundations of Cryptographyの著者であるOded Goldreichです。^[25]彼は、彼らの最初の論文「「証明可能なセキュリティ」の別の見方」^[26]に対する反論を執筆し、「ポストモダン暗号について」と題しました。ゴールドライヒは次のように書いている。「...我々は、この論文の根底にある根本的な哲学的欠陥と、過去四半世紀における暗号理論研究に関する誤解のいくつかを指摘する。」^{[27] : 1}ゴールドライヒは論文の中で、証明可能なセキュリティの厳密な分析方法論だけが科学と両立するものであり、コブリッツとメネゼスは「反動主義者（つまり、進歩の反対者の思うつぼだ）」であると主張した。^{[27] : 2}

2007年、コブリッツは「数学と暗号の不安定な関係」^[28]を出版したが、そこには証明可能なセキュリティやその他の話題に関する物議を醸す発言が含まれていた。研究者のオデッド・ゴールドライヒ、ボアズ・バラク、ジョナサン・カッツ、ヒューゴ・クラフチク、アヴィ・ウィグダーソンは、コブリッツの記事に対する返答の手紙を書き、その手紙は2007年11月号と2008年1月号の同誌に掲載された。^{[29] [30]} 暗号学の教科書の共著者であるカッツは^[31]、コブリッツの記事を「最も純粋なスノッブ」と呼んだ。^{[29] : 1455}また、プリンストン高等研究所の常任理事であるウィグダーソンは、コブリッツを「中傷」で非難した。^{[30] : 7}

イヴァン・ダムゴードは後にICALP 2007で技術的な問題に関する立場表明を執筆し^[32]、スコット・アーロンソンはそれを優れた詳細な分析として推奨した。^[33]米国 国家安全保障局情報保証局の元技術ディレクターであるブライアン・スノーは、コブリッツ＝メネゼスの論文「暗号における大胆な仮定のすばらしい新世界」^[34]をRSAカンファレンス2010暗号専門家パネルの聴衆に推奨した。^[35]

古典的な証明可能セキュリティは、主に漸近的に定義されたオブジェクト間の関係を研究することを目的としています。一方、実践指向の証明可能セキュリティは、ハッシュ関数、ブロック暗号、プロトコルなどの暗号実践の具体的なオブジェクトが展開され使用される際に関係します。^[36]実践指向の証明可能セキュリティは、固定キーサイズの実用的な構造を分析するために具体的なセキュリティを使用します。「正確なセキュリティ」または「具体的なセキュリティ」は、セキュリティパラメータの「十分に大きい」値に対して保持されることが保証されている漸近的な境界ではなく、計算努力の正確な境界を計算することによってセキュリティを定量化する証明可能セキュリティ削減に付けられた名前です。