2つのモデルの物語：Tamarinを用いたKEMTLSの形式的検証

概要

KEMTLSは、後量子アルゴリズムの特性におけるトレードオフを考慮して、署名ではなく長期的なキーエンキャプセル化メカニズムのキーを用いてハンドシェイクを認証するための提案です。KEMTLSおよびその変種KEMTLS-PDKのセキュリティに関する既存の証明は、計算的仮定の下で還元主義的モデルで手書きで行われました。本論文では、2つの異なるTamarinモデルを用いてKEMTLSとKEMTLS-PDKのコンピュータ検証済みの記号的分析を提示します。最初の分析では、Cremersら（ACM CCS 2017）が作成したTLS 1.3の詳細なTamarinモデルを、プロトコル仕様のワイヤーフォーマットに密接に従うように変更し、KEMTLS（-PDK）に適応させました。このモデルにおいて、KEMTLS（-PDK）がTLS 1.3と同一のセキュリティ特性を持っていることを示します。このTamarin証明は前回のTLS 1.3 Tamarinモデルと比較して完全に自動化可能であり、前回のモデルでは大きな手作業が必要でしたが、そのモデルにいくつかの不整合が見つかりました。2番目の分析では、KEMTLS（-PDK）の新しいTamarinモデルを提示します。これは、従来の紙と鉛筆によるKEMTLS（-PDK）の証明で使用されたマルチステージキーエクスチェンジセキュリティモデルに密接に従います。2番目のアプローチはプロトコル仕様のワイヤーフォーマットからさらに離れているものの、否認可能性や異なるレベルのフォワードシークレシーなどのセキュリティ定義のより詳細な側面を捉えています。また、紙と鉛筆による証明におけるセキュリティ主張のいくつかの欠陥を特定しています。我々のポジティブなセキュリティ結果は、KEMTLS（-PDK）の設計への信頼を高めます。さらに、これらのモデルを並べて見ることで、プロトコル仕様の詳細さとセキュリティ特性の粒度の間の記号的分析におけるトレードオフについてコメントできます。