Leanによる形式検証入門 Part 1

インサイトに戻るインサイトに戻るチュートリアル: Leanによる形式検証入門 (Part 1)ElenaCryptography Engineer2026年7月15日形式検証とは、(数学的な)命題の正しさを検証するためのツールです。ペンと紙で数学の証明を書く代わりに、形式検証ツールを使って証明をコードで記述し、機械でチェックすることで、証明が正しいことを確実に知ることができます。これらのツールの例としては、Rocq (形式的にはCoq)、Isabelle、そしてこのチュートリアルのトピックであるLeanがあります。 このチュートリアルでは、暗号化に関する簡単な命題とその証明をLeanで記述します。したがって、形式検証の初心者や、形式検証の基本知識を復習したい暗号技術者にとって楽しいものとなることを目指します。 具体的には、Leanの非常に基本的な部分をウォークスルーし、その後、最初にClaude Shannonによって普及しましたが、Frank MillerとGilbert Vernamによって以前に説明されたワンタイムパッド(OTP)プロトコルを形式的に検証します。 このチュートリアルの目標は、ワンタイムパッドのような、より単純な暗号プロトコルに関する形式的な定義と証明を取得し、Leanに移植することです。定義と証明の主な情報源として、Dan BonehとVictor Shoupの "A Graduate Course in Applied Cryptography" を使用します。 このチュートリアルの終わりまでには、VCV-ioのような他の形式化された暗号化のLean証明を調べることができるようになるはずです。 免責事項: これはLeanにおけるベストプラクティスを与えるものでは決してなく、むしろ暗号技術者にとって意味があり、楽しめるような入門となることを意図しています。 Leanプログラミング言語 & 証明支援系 Leanは2013年にMicrosoft ResearchのLeonardo de Mouraによって作成されました。これは関数型プログラミング言語であり、定理証明器です。 数学者は、公理、補題、定理を記述し、必要に応じて証明を追加するためにこれを使用できます。証明がLeanによってコンパイルされた場合、それは正しいことを意味します (Leanコンパイラへの信頼を前提とします)。検証可能な証明という利点に加えて、証明をサブ証明に分割しやすく、共同作業も容易になります。さらに、Leanは欠落している部分を自動的に検索して適用することで、証明の完了を支援できます。 しかし、Leanは「単なる」プログラミング言語でもあります。具体的には、純粋関数型プログラミング言語であり、プログラムに副作用がなく、関数が第一級の値として扱われることを意味します。後者については、チュートリアルでさらに詳しく見ていきます。 Leanを始めるための素晴らしいリソースはたくさんあります。いくつか紹介します: 初心者向けの書籍と演習: The Hitchhiker’s Guide to Logical Verification Leanウェブサイトの入門書: Functional Programming in Lean. 関数型プログラミングの知識がある場合は素晴らしいでしょう。 Theorem Proving in Lean 4. より数学的な目的。 Natural Numbers Game. ブラウザで直接Leanでの証明を学ぶためのインタラクティブなゲーム。 (多くの素晴らしいリソースがすでに存在しているにもかかわらず、この特定の演習を作成した理由は、暗号化との特定の重複があるためです。VCV-ioは暗号化に関する素晴らしい証明を持っていますが、初心者には難しすぎ、チュートリアルがありません。) チュートリアル 始めましょう。チュートリアルは、「Hello World!」を簡単に実行した後、4つのパートに分かれています (パート2が最も長いです)。すべてLean 4で行われ、コードを一緒に書くことを想定しています。 行番号付きで表示されるコードは、最終結果に必要なコードです。行番号のないコードは、まだ完了していないか、何かを確認するためだけのものですので、安全に削除できます。 最後に、セクションの先頭には、そのセクションで共有される新しい概念を含む小さなコメントがあります。 LeanでのHello World Lean InfoView eval Leanをローカルにダウンロードするか、https://live.lean-lang.org/ のようなオンラインエディタを使用できます。これは以下のような見た目になります。左側でLeanを書き、右側は有用な情報やヒントが表示されるLean InfoViewです。 すべてが正常に機能することを確認するために、次のようなものを記述します: #eval 1+1 そして、結果が右側のInfoViewに表示されることを確認してください。 伝統的な「Hello World!」のために、次のいずれかを行うことができます: #eval "Hello World!" #eval String.append "Hello " "World!" #eval String.append "Hello " (if 1 > 2 then "Lean!" else "World!") Leanのいくつかのプロパティ: 標準的な数学的慣習に従います。例: #eval 4 + 5 * 6 は 4+(5*6)=34 と評価されます。 関数引数を保持するための括弧はありません。つまり、Leanでは f(x) の代わりに f x と記述します。 関数はLeanの第一級の値です。数値や文字列のような値と同じように扱われます。 しかし、先走りすぎないようにしましょう。必要なLeanのトピックは、進むにつれて学んでいきます。 本は何と言っているか？つまり、Leanに移植したいものは何か？ 何を定義したいかは多かれ少なかれわかっていますが、Leanを使用する上での要点は、明確さと精度が必要であるということです。具体的に何を定義したいのか、そしてそれをどのように定義するのか？だからこそ、Boneh & Shoupの本を使用するのです。必要な数学はすでに書き出されているので、Leanへの翻訳だけを心配すればよいのです。 まず、シャノン暗号 (2.1.1) の定義があり、それは3つのプロパティを持っています。最初の2つは暗号化関数と復号化関数が何であるかを述べ、最後の1つは正しさのプロパティであり、暗号化の後に復号化を行うと元のメッセージが返されることを示しています。 私たちが興味を持っている具体的な例はワンタイムパッドであり、暗号化と復号化は単純にXOR演算です: チュートリアルのかなりの部分を、ビット単位の排他的論理和 (XOR) のプロパティを証明することに費やします: そして最後に、ワンタイムパッドがシャノン暗号であること、つまり正しさのプロパティを満たすことを証明できます: この最初のチュートリアルでは、次の簡単なステップを実行します: ビット文字列とXOR関数を定義する XORの必要なプロパティを証明する (可換性、結合性、単位元、自己逆元) 暗号化関数、復号化関数、そして復号化が暗号化を「逆転させる」プロパティ (正しさ) を持つシャノン暗号を定義する 暗号化と復号化がXORであるOTPがシャノン暗号であることを示す 準備はできましたか？始めましょう。 チュートリアル Part 1: BitString と XOR を定義する ワンタイムパッドは、キーK、メッセージM、暗号文Cすべてが同じ長さLのビット文字列であると定義されます。K := M := C := {0,1}ᴸ。 XORの定義では、2を法とする加算が必要です。したがって、{0,1}ᴸをℤ₂ᴸとして扱い、Leanでℤ₂上の算術を使用すると役立ちます。 有限体 ライブラリをインポートする Zmod n まず、Leanの数学ライブラリから有限体ライブラリZModをインポートします: import Mathlib.Data.ZMod.Basic この事前定義されたライブラリZMod nは、モジュラ算術があらかじめ実装されている整数 modulo n を定義します。(Cmd/Ctrl + クリックで、実装済みの型についてさらに詳しく読むことができます。例えば、ZMod nを確認してください。) ZModに慣れるために、簡単なモジュラ算術を試してみてください。例えば、5 + 6 mod 7: #eval (5: ZMod 7) + (6: ZMod 7) これで、ZMod 2の要素のベクトルとして、新しい型を作成することにより、K、M、Lのドメインを定義できます。 BitStringの定義 Vector 依存型チェック Leanの良い点は、ビット文字列の長さLを固定する必要がないことです。数学で書くように、単にLをℕとして指定できます。(Leanでℕを書くには、「 」と入力します。) 定義済みの型Vector α nは、長さnで型αの要素を持つベクトルを作成します。したがって、カスタム型ℤ₂ᴸを定義するためにVector (ZMod 2) Lを使用できます: 1def BitString (L: ℕ): Type := Vector (ZMod 2) L これは依存型であり、ℕの異なる値に対して異なるインスタンス化を提供します。確認できます: -- Leanではコメントを--で始めます #check BitString 5 --BitString 5 : Type #eval は何も評価するものがないため機能しませんが、#check は式の型を表示します。この場合、うまく機能します。 XORの定義 暗黙的なパラメータ カリー化 ラムダ関数 次に、ビット文字列x = [x_1, …, x_L]とy = [y_1, …, y_L]を入力として、XOR関数を[x_1 +₂ y_1, …, x_L +₂ y_L]と定義します。ここで+₂は2を法とする加算です。 Leanでこれをどのように定義できるでしょうか？数学での関数シグネチャを考えてみましょう: ℤ₂ᴸ × ℤ₂ᴸ → ℤ₂ᴸ。これを実現するにはいくつかの方法があります。