暗号化プロトコル

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

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

• 重要な合意または確立
• エンティティ認証
• 対称暗号化とメッセージ認証の マテリアル構築
• 安全なアプリケーションレベルのデータ転送
• 否認防止方法
• 秘密共有法
• 安全なマルチパーティ計算

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

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

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

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

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

• バロウズ・アバディ・ニーダム論理（BAN論理）
• Dolev-Yao モデル
• π計算
• プロトコル構成ロジック (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]

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

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

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

• インターネット鍵交換
• IPsec
• ケルベロス
• 非公式メッセージ
• ポイントツーポイントプロトコル
• セキュア シェル(SSH)
• 信号プロトコル
• トランスポート層セキュリティ
• ＺＲＴＰ

• 暗号システムの一覧
• 安全なチャネル
• セキュリティ プロトコル オープン リポジトリ
• 暗号化ライブラリの比較

• Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (2016 年 9 月)。「エンドツーエンド暗号化メッセージング プロトコル: 概要」( PDF)。Bagnoli, Franco 他 (編)。インターネットサイエンス。INSCI 2016。フィレンツェ、イタリア: Springer。pp. 244–254。doi :10.1007/978-3-319-45982-0_22。ISBN 978-3-319-45982-0。