Lean으로 암호학 증명을 자동 검증하는 튜토리얼: One-Time Pad 사례로 배우는 형식 검증
Introduction to Formal Verification with Lean Part 1
HashCloak이 Lean 4를 사용한 형식 검증(formal verification) 입문 튜토리얼을 공개했다. 이 튜토리얼은 암호 엔지니어를 대상으로 하며, 기본적인 Lean 문법부터 시작해 One-Time Pad(OTP) 프로토콜의 정확성을 기계적으로 증명하는 과정을 안내한다. Boneh와 Shoup의 'A Graduate Course in Applied Cryptography'를 참고해 Shannon cipher 정의와 XOR의 교환법칙·결합법칙·항등원·자기상반성 등을 증명하고, OTP가 Shannon cipher임을 보여준다. 코드를 직접 따라 하며 배울 수 있도록 설계되었으며, VCV-io의 고급 증명으로 나아가기 위한 발판을 제공한다.
형식 검증은 (수학적) 명제의 정확성을 검증하는 도구로, 우리가 종이와 펜으로 수학 증명을 쓰는 대신 코드로 증명을 작성하고 기계가 검증하게 하여 증명이 확실히 맞는지 알 수 있게 해줍니다.