Leanを用いた暗号プロトコルの形式検証入門

形式検証はLean言語を使用して暗号プロトコルの正確性を数学的に証明するための手法である。HashCloakによる新しいチュートリアルは、ワンタイムパッドプロトコルを例に、Leanでの定義と証明方法を段階的に解説する。

形式検証の基礎と、ワンタイムパッド暗号の性質をLean 4で証明するチュートリアル。XOR演算の可換性と結合法則、単位元、自己逆元などの性質を形式的に検証する方法を紹介している。

形式検証とLean言語

「形式検証は（数学的）ステートメントの正確性を検証するツールである」とチュートリアルは述べている。Leanは2013年にMicrosoft Researchに所属していたLeonardo de Mouraによって開発された関数型言語兼定理証明器である。Leanは純粋関数型プログラミング言語であり、プログラムには副作用がない。「Leanコンパイラによってプルーフがコンパイルされるならば、それは正しい（Leanコンパイラへの信頼を前提として）」とされている。

チュートリアルの構成と対象範囲

チュートリアルはワンタイムパッドプロトコルを形式検証する方法を段階的に説明する。ビット文字列の定義、XOR関数の実装、およびXOR演算の複数の性質の証明を含む。加えて、Shannon暗号構造の定義も扱っている。Dan BonehとVictor Shoupの『A Graduate Course in Applied Cryptography』から定義と証明の根拠を得ている。

ワンタイムパッドプロトコルの背景

ワンタイムパッドプロトコルはClaude Shannonによって最初に普及させられたが、Frank MillerとGilbert Vernamによってさらに早期に記述されていた。チュートリアルではこのプロトコルの数学的性質をLeanで厳密に証明することで、暗号プロトコルの形式検証の実践方法を示している。

ビット文字列とXOR演算の実装

ビット文字列はVector (ZMod 2) Lにより定義される。XOR関数はVector.zipWithと2を法とした加算を使用して実装される。Vector.replicate L 0は長さLで0で埋められたビット文字列を生成する。CharTwo.add_eq_zeroは特性2環においてa + b = 0 ↔ a = bを示す定理である。

筆者の見立て

• このチュートリアルは、形式検証に初めて取り組む暗号技術者にとって実用的で有用であることを意図していると論じている。
• 形式検証の最良実践を提供することではなく、暗号技術者にとって理解しやすく有用な入門を目指していると解釈している。

この記事は元記事の事実のみに基づいて自動生成されました。

出典

HashCloak、"Tutorial: Introduction to Formal Verification with Lean (Part 1) - HashCloak"、https://hashcloak.com/blog/tutorial-introduction-to-formal-verification-with-lean-(part-1)