用Lean形式化验证One-Time Pad

Introduction to Formal Verification with Lean Part 1

形式化验证让数学证明从纸笔走向代码，通过机器检查确保绝对正确。本文以Lean为工具，手把手带你从零开始，将Dan Boneh和Victor Shoup的经典密码学教材中的One-Time Pad协议进行形式化验证。我们将定义BitString和XOR运算，证明其交换律、结合律等关键性质，并最终验证One-Time Pad符合Shannon Cipher的正确性要求。无论是对形式化验证好奇的密码学工程师，还是想重温基础的新手，这篇教程都能让你在编码中体验数学证明的严谨与乐趣。