論文の概要: Computationally Bounded Robust Compilation and Universally Composable Security
- arxiv url: http://arxiv.org/abs/2401.15041v1
- Date: Fri, 26 Jan 2024 18:09:47 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-18 08:07:41.674959
- Title: Computationally Bounded Robust Compilation and Universally Composable Security
- Title（参考訳）: 計算境界付きロバストコンパイルとユニバーサル構成可能なセキュリティ
- Authors: Robert Künnemann, Marco Patrignani, Ethan Cecchetti,
- Abstract要約: ユニバーサル・コンポータビリティ(Universal Composability、UC)は、暗号セキュリティの標準規格である。
UCはツールの検証が難しいことで知られている。
リアルメカニカルな平等結果。
- 参考スコア（独自算出の注目度）: 7.284860523651358
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure. This paper addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC$\unicode{x2013}$RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CryptoVerif to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL.
- Abstract（参考訳）: ユニバーサル・コンポータビリティ(UC)は暗号セキュリティの金の標準であるが、UCの機械化は極めて難しい。
UCとRobust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to confirmed UC proofs using tools that mechanizing equality results。
残念ながら、既存の手法は完全なUCセキュリティにのみ適用され、暗号に依存する現実世界のプロトコルは計算的にのみ安全である。
本稿では,UC と RC の接続を計算環境に引き上げることにより,このギャップに対処する。
さらに、UC$\unicode{x2013}$RC接続は計算セキュリティを超えて任意の等式に一般化され、既存の完全ケースを仮定し、より複雑なセキュリティ概念で将来の理論をインスタンス化するためのフレームワークを提供する。
この接続により、コンピュータのUCセキュリティの証明を適切に機械化するための計算不可能性の証明のためのツールを使用することができる。
我々は、CryptoVerifを使用して、Wireguardプロトコルの一部がコンピュータでセキュアであることを示す。
最後に、フレームワーク自体のすべての証明は、Isabelle/HOLで検証される。
関連論文リスト
- Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
認証サイクル冗長性チェック(ACRIC)を提案する。
ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。
ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
論文 参考訳（メタデータ） (2024-11-21T18:26:05Z) - At Least Factor-of-Two Optimization for RWLE-Based Homomorphic Encryption [0.0]
ホモモルフィック暗号化(HE)は、復号化を必要とせずに、暗号化データの特定の操作をサポートする。
HEスキームには、データ集約的なワークロードを妨げるような、非自明な計算オーバーヘッドが伴います。
我々は、Zincと呼ぶ暗号化方式を提案し、複数のキャッシュ処理を禁止し、単一のスカラー加算で置き換える。
論文 参考訳（メタデータ） (2024-08-14T05:42:35Z) - Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
我々は、新しいハイブリッドユニバーサルネットワーク符号化暗号(NU-HUNCC)を導入する。
NU-HUNCCは,リンクのサブセットにアクセス可能な盗聴者に対して,個別に情報理論的に保護されていることを示す。
論文 参考訳（メタデータ） (2024-02-13T12:12:39Z) - SECOMP: Formally Secure Compilation of Compartmentalized C Programs [2.5553752304478574]
C言語の未定義の動作は、しばしば破壊的なセキュリティ脆弱性を引き起こす。
本稿では,機械チェックによるC言語のコンパイラSECOMPを紹介する。
このような強い基準が主流のプログラミング言語で証明されたのは、これが初めてです。
論文 参考訳（メタデータ） (2024-01-29T16:32:36Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
信頼性コンピューティングは、Trusted Execution Environments(TEEs)と呼ばれる特別なハードウェア隔離ユニットを使用して、コテナントクラウドデプロイメントにおける機密コードとデータの保護を可能にする。
低レベルのC/C++ベースのツールチェーンを提供するTEEは、固有のメモリ安全性の脆弱性の影響を受けやすく、明示的で暗黙的な情報フローのリークを監視するための言語構造が欠如している。
私たちは、Haskellに埋め込まれたドメイン固有言語(cla)であるHasTEE+を使って、上記の問題に対処します。
論文 参考訳（メタデータ） (2024-01-17T00:56:23Z) - Secure Synthesis of Distributed Cryptographic Applications (Technical Report) [1.9707603524984119]
我々はセキュアなプログラムパーティショニングを用いて暗号アプリケーションを合成することを提唱する。
このアプローチは有望だが、そのようなコンパイラのセキュリティに関する公式な結果はスコープに限られている。
我々は、堅牢で効率的なアプリケーションに不可欠な微妙さを扱うコンパイラのセキュリティ証明を開発した。
論文 参考訳（メタデータ） (2024-01-06T02:57:44Z) - SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
本稿では,SOCIの性能を大幅に向上させるSOCI+を提案する。
SOCI+は、暗号プリミティブとして、高速な暗号化と復号化を備えた(2, 2)ホールドのPaillier暗号システムを採用している。
実験の結果,SOCI+は計算効率が最大5.4倍,通信オーバヘッドが40%少ないことがわかった。
論文 参考訳（メタデータ） (2023-09-27T05:19:32Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z) - Mitigating Leakage in Federated Learning with Trusted Hardware [0.0]
連合学習では、複数のパーティが協力して、それぞれのデータセット上でグローバルモデルをトレーニングします。
不正に行われた場合、一部の情報はまだ関係者間でリークされる可能性がある。
信頼性の高い実行環境に依存した2つのセキュアバージョンを提案する。
論文 参考訳（メタデータ） (2020-11-10T07:22:51Z) - Quantum copy-protection of compute-and-compare programs in the quantum random oracle model [48.94443749859216]
計算・比較プログラム(Computer-and-compare program)として知られる回避関数のクラスに対する量子コピー保護スキームを導入する。
我々は,量子乱数オラクルモデル(QROM)において,完全悪意のある敵に対する非自明なセキュリティを実現することを証明した。
補完的な結果として、「セキュアソフトウェアリース」という,ソフトウェア保護の概念の弱さが示される。
論文 参考訳（メタデータ） (2020-09-29T08:41:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。