暗号化プロトコル

暗号プロトコルとは、セキュリティ関連の機能を実行し、暗号手法（多くの場合、暗号プリミティブのシーケンスとして）を適用する抽象的または具体的なプロトコルです。プロトコルは、アルゴリズムの使用方法を記述し、データ構造と表現に関する詳細を含みます。これにより、プログラムの複数の相互運用可能なバージョンを実装することができます。^[1]

暗号化プロトコルは、アプリケーションレベルの安全なデータ転送に広く利用されています。暗号化プロトコルには通常、少なくとも以下の要素が組み込まれています。

重要な合意または確立
エンティティ認証（認証プロトコルを使用する場合もある）
対称暗号化とメッセージ認証の鍵マテリアルの構築
安全なアプリケーションレベルのデータ転送
否認防止方法
秘密分散法
安全なマルチパーティ計算

例えば、トランスポート層セキュリティ（TLS）は、Web（ HTTPS）接続のセキュリティ確保に使用される暗号化プロトコルです。 ^{[2] TLSは、}X.509システムに基づくエンティティ認証メカニズム、公開鍵暗号を用いて対称暗号鍵を生成する鍵設定フェーズ、そしてアプリケーションレベルのデータ転送機能を備えています。これら3つの側面は重要な相互関係を持っています。標準的なTLSには否認防止機能は備わっていません。

暗号プロトコルには他にも様々な種類があり、その用語自体にも様々な読み方があります。暗号アプリケーションプロトコルは、多くの場合、1つ以上の基盤となる鍵共有方式を採用しており、これらの方式自体も「暗号プロトコル」と呼ばれることがあります。例えば、TLSはDiffie-Hellman鍵交換と呼ばれる方式を採用しています。これはTLS自体の一部に過ぎませんが、他のアプリケーションではDiffie-Hellman自体が完全な暗号プロトコルとみなされることもあります。

高度な暗号化プロトコル

多種多様な暗号プロトコルは、データの機密性、整合性、認証といった従来の目標を超え、コンピュータを介したコラボレーションにおける様々な望ましい特性も保護します。^[3] ブラインド署名は、デジタルキャッシュやデジタルクレデンシャルにおいて、ある人物の身元や取引相手の身元を明かすことなく、ある人物が属性や権利を有していることを証明するために使用できます。安全なデジタルタイムスタンプは、データ（機密データであっても）が特定の時間に存在したことを証明するために使用できます。安全なマルチパーティコンピューティングは、機密データ（非公開入札など）に基づいて回答（オークションでの最高入札額の決定など）を計算するために使用できます。これにより、プロトコルが完了すると、参加者は自分の入力と回答のみを知ることができます。エンドツーエンドで監査可能な投票システムは、電子投票を実施するための望ましいプライバシーと監査可能性のプロパティを提供します。否認不可能な署名には、署名者が偽造を証明し、署名を検証できる人物を制限できる対話型プロトコルが含まれます。否認可能な暗号化は、攻撃者が平文メッセージの存在を数学的に証明することを不可能にすることで、標準的な暗号化を補強します。デジタルミックスは、追跡が困難な通信を実現します。

形式検証

暗号プロトコルは、抽象的なレベルで形式的に検証できる場合があります。検証を行う場合、脅威を特定するために、プロトコルが動作する環境を形式化する必要があります。これは、Dolev-Yaoモデルを通じて行われることがよくあります。

セキュリティプロトコルの形式的推論に使用されるロジック、概念、計算:

セキュリティプロトコルの形式検証に使用される研究プロジェクトとツール:

インターネットセキュリティプロトコルとアプリケーションの自動検証（AVISPA）と後継プロジェクトAVANTSSAR。^[5]^[6]
- 制約論理ベースの攻撃探索器（CL-AtSe）^[7]
- オープンソース固定小数点モデルチェッカー（OFMC）^[8]
- SATベースモデルチェッカー（SATMC）^[9]
キャスパー^[10]
クリプトベリフ
暗号プロトコル形状アナライザー（CPSA）^[11]
セキュリティプロトコルに関する知識（KISS）^[12]
Maude-NRLプロトコルアナライザ（Maude-NPA）^[13]
プロベリフ
サイヤ人^[14]
タマリン・プルーバー^[15]
リス^[16]

抽象プロトコルの概念

プロトコルを形式的に検証するために、多くの場合、アリス・ボブ記法を用いて抽象化されモデル化されます。簡単な例を以下に示します。

A\rightarrow B:\{X\}_{K_{A,B}}

これは、アリスが共有キーで暗号化されたメッセージで構成されるボブへのメッセージを意図していることを示しています。 $A$ $B$ $X$ $K_{A,B}$

例

参照

参考文献

^ 「暗号化プロトコルの概要」（PDF） 2015年10月23日. 2017年8月29日時点のオリジナル（PDF）からアーカイブ。 2015年10月23日閲覧。
^ チェン、シャン;ジェロ、サミュエル。ジャギエルスキー、マシュー。ボルディレヴァ、アレクサンドラ。ニタ・ロタル、クリスティーナ（2021-07-01）。「安全な通信チャネルの確立: TLS 1.3 (over TCP Fast Open) と QUIC」。暗号学ジャーナル。34 (3): 26.土井: 10.1007/s00145-021-09389-w。ISSN 0933-2790。S2CID 235174220。
^ Berry Schoenmakers. 「暗号化プロトコルに関する講義ノート」(PDF) .
^ Fábrega、F. Javier Thayer、Jonathan C. Herzog、および Joshua D. Guttman、Strand Spaces: セキュリティプロトコルが正しい理由{{citation}}: CS1 maint: multiple names: authors list (link)
^ “Automated Validation of Internet Security Protocols and Applications (AVISPA)”. 2016年9月22日時点のオリジナルよりアーカイブ。2024年2月14日閲覧。
^ Armando, A.; Arsac, W; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y.; +12 more (2012). Flanagan, C.; König, B. (eds.). The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. Vol. 7214. LNTCS. pp. 267– 282. doi :10.1007/978-3-642-28756-5_19 . 2024年2月14日閲覧。{{cite book}}: CS1 maint: numeric names: authors list (link)
^ 「制約論理ベースの攻撃サーチャー（Cl-AtSe）」。2017年2月8日時点のオリジナルよりアーカイブ。2016年10月17日閲覧。
^ オープンソース固定小数点モデルチェッカー (OFMC)
^ 「セキュリティプロトコルとセキュリティに配慮したアプリケーションのためのSATベースモデルチェッカー（SATMC）」。2015年10月3日時点のオリジナルよりアーカイブ。2016年10月17日閲覧。
^ Casper: セキュリティプロトコル解析用コンパイラ
^ cpsa: シンボリック暗号プロトコルアナライザー
^ “Knowledge In Security protocolS (KISS)”. 2016年10月10日時点のオリジナルよりアーカイブ。2016年10月7日閲覧。
^ Maude-NRL プロトコルアナライザ (Maude-NPA)
^ ストライカー
^ タマリン・プルーバー
^ リスの証明者

さらに読む

エルモシナ, クセニア; ムシアニ, フランチェスカ; ハルピン, ハリー (2016年9月). 「エンドツーエンド暗号化メッセージングプロトコル：概要」(PDF) . Bagnoli, Franco他編. Internet Science . INSCI 2016. フィレンツェ, イタリア: Springer. pp. 244– 254. doi :10.1007/978-3-319-45982-0_22. ISBN 978-3-319-45982-0。