Leanでワンタイムパッドの正しさを機械検証するチュートリアル

Introduction to Formal Verification with Lean Part 1

HashCloakのチュートリアルでは、定理証明支援系Leanを使って暗号プロトコルの形式的検証を始める方法を解説します。Leanの基本を学びながら、ワンタイムパッド（OTP）がShannon暗号の正しさの性質を満たすことを証明します。XORの可換性や結合性などの性質をLeanで証明し、Boneh-Shoupの教科書の定義をLeanに移植する手法を紹介します。暗号技術者向けに、形式的検証の基礎を実践的に学べる内容です。