暗号プロトコル

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

暗号化プロトコルは、アプリケーションレベルの安全なデータ転送に広く用いられています。暗号化プロトコルは通常、少なくとも以下の要素の一部を備えています。

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

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

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

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

暗号プロトコルは、抽象的なレベルで形式的に検証できる場合がある。検証を行う際には、脅威を特定するために、プロトコルが動作する環境を形式化する必要がある。これは、多くの場合、ドレフ＝ヤオモデルを用いて行われる。

セキュリティプロトコルの形式的推論に使用される論理、概念、および計算体系：

• バロウズ・アバディ・ニーダム論理（BAN論理）
• ドレフ・ヤオモデル
• π計算
• プロトコル合成ロジック（PCL）
• ストランド空間^{[ 4 ]}

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

• インターネットセキュリティプロトコルとアプリケーションの自動検証（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 ]}
• StrandsRocq ^{[ 17 ]}

• インターネット鍵交換
• IPsec
• ケルベロス
• 非公式メッセージ
• ポイントツーポイントプロトコル
• セキュアシェル（SSH）
• シグナルプロトコル
• トランスポート層セキュリティ
• ZRTP

• 暗号システム一覧
• セキュアチャネル
• セキュリティプロトコル公開リポジトリ
• 暗号化ライブラリの比較
• 量子暗号プロトコル

• エルモシナ、クセニア；ムシアニ、フランチェスカ；ハルピン、ハリー（2016年9月）「エンドツーエンド暗号化メッセージングプロトコル：概要」（PDF）バニョーリ、フランコ他 編『インターネットサイエンス』INSCI 2016、フィレンツェ、イタリア：スプリンガー、pp. 244–254、doi：10.1007/978-3-319-45982-0_22、ISBN  978-3-319-45982-0。