Формальная верификация позволяет проверить корректность математических утверждений с помощью машинной проверки доказательств. В этом туториале её применяют к криптографии — на примере шифра одноразового блока (One-Time Pad, OTP), используя ассистент доказательств Lean (создан в 2013 году Леонардо де Моурой в Microsoft Research). Автор опирается на определения из книги Boneh & Shoup «A Graduate Course in Applied Cryptography». Цель — перевести формальные определения и доказательства OTP в код Lean.
Сначала импортируется библиотека ZMod для работы с модульной арифметикой: import Mathlib.Data.ZMod.Basic. Тип BitString L определяется как Vector (ZMod 2) L — вектор длины L над полем ℤ₂. Функция XOR реализуется через Vector.zipWith (fun a b => a + b). Для избежания конфликта имён перед определением ставят set_option pp.structure_projections false.
Дальше идут доказательства свойств XOR. Коммутативность (xor x y = xor y x) доказывается с помощью Vector.ext, затем intro i h_i_lt_L и simp [xor, add_comm]. Ассоциативность (xor x (xor y z) = xor (xor x y) z) — аналогично, но с add_assoc. Для identity создаётся BitString_ID := Vector.replicate L 0, и свойство xor x BitString_ID = x доказывается через Vector.ext fun i i_less_than_L => by simp [xor, BitString_ID]. Самобратность (xor x x = BitString_ID) требует CharTwo.add_eq_zero.mpr rfl, так как в ℤ₂ a + a = 0 равносильно a = a.
Затем определяется структура ShannonCipher с полями encrypt, decrypt и свойством корректности: decrypt k (encrypt k m) = m. Для OTP, где ключи, сообщения и шифротексты — битовые строки одинаковой длины, а операции — XOR, достаточно доказать это свойство, используя уже доказанные свойства XOR (в частности, xor_self_inverse и xor_show_identity). Весь код написан на Lean 4.
Туториал разбит на четыре части, самая длинная — вторая (доказательства свойств XOR). Он ориентирован на криптографов, начинающих знакомство с формальной верификацией. После его прохождения читатель сможет разбирать более сложные формальные доказательства, например от проекта VCV-io.