暗号化クライアントハロを用いたTLS 1.3のプライバシーの記号的分析

概要

TLS 1.3は、トランスポートレイヤーセキュリティ（TLS）プロトコルの最新バージョンであり、強力な認証および機密性の保証を提供しています。これらは、さまざまな形式モデルで包括的に分析されています。しかし、ハンドシェイクのメタデータ暗号化の批判的な使用にもかかわらず、TLS 1.3のプライバシー保証は依然として弱く、十分に理解されていません。たとえば、プロトコルはネットワーク攻撃者にターゲットサーバーの識別情報を明らかにし、TLS接続の受動的な監視およびアクティブな検閲を可能にします。このギャップを埋めるために、IETF TLS作業部会は、暗号化クライアントハロ（Encrypted Client Hello、通称ECN）という新しいプライバシー拡張を標準化していますが、形式的なプライバシーモデルの欠如により、この拡張が動作することを検証することが難しいです。実際、ECNのいくつかの初期ドラフトは、アクティブなネットワーク攻撃に対して脆弱であることが判明しています。 本論文では、TLS 1.3ハンドシェイクのプライバシー特性の最初の機械化された形式的な分析を提示します。私たちは、ProVerifという記号的プロトコルアナライザを使用して、TLS 1.3のすべての標準モード（ECNを含む/含まない）を研究します。ECNの攻撃について議論し、本研究の過程で発見されたものも含め、それらが最新バージョンでどのように考慮されているかを示します。我々の分析はECNの標準化プロセスを支援し、TLS実装者向けの具体的なプライバシーの推奨事項を提供します。また、プロトコルに新しい拡張機能を試みるデザイナーが使用できる、現在までで最も包括的なTLS 1.3モデルを提供します。我々の分析は、自動検証ツールを使用して試みられた最大規模のプライバシー証明の一つであり、プロトコルアナリストにとって一般的な関心事である可能性があります。