Cryptographic protocol

A cryptographic protocol is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol describes how the algorithms should be used and includes details about data structures and representations, at which point it can be used to implement multiple, interoperable versions of a program.^[1]

Cryptographic protocols are widely used for secure application-level data transport. A cryptographic protocol usually incorporates at least some of these aspects:

• Key agreement or establishment
• Entity authentication, perhaps using an authentication protocol
• Symmetric encryption and message authenticationkey material construction
• Secured application-level data transport
• Non-repudiation methods
• Secret sharing methods
• Secure multi-party computation

For example, Transport Layer Security (TLS) is a cryptographic protocol that is used to secure web (HTTPS) connections.^[2] It has an entity authentication mechanism, based on the X.509 system; a key setup phase, where a symmetric encryption key is formed by employing public-key cryptography; and an application-level data transport function. These three aspects have important interconnections. Standard TLS does not have non-repudiation support.

There are other types of cryptographic protocols as well, and even the term itself has various readings; Cryptographic application protocols often use one or more underlying key agreement methods, which are also sometimes themselves referred to as "cryptographic protocols". For instance, TLS employs what is known as the Diffie–Hellman key exchange, which although it is only a part of TLS per se, Diffie–Hellman may be seen as a complete cryptographic protocol in itself for other applications.

さまざまな暗号プロトコルは、データの機密性、完全性、認証という従来の目標を超えて、コンピュータを介したコラボレーションのさまざまな望ましい特性も保護します。^{[ 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

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

• 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。