以前ワンタイムパッド暗号を紹介し、その完全秘匿性をLean4で形式証明しました。暗号の定義の中で「使った鍵は再利用してはいけない」、ということを書きました。ただしその条件は証明の中で明示的に使われているようには見えないし、数学的な条件なのか一般…

最近の記事では暗号とその安全性証明の基礎を勉強したいと思い、シャノンの完全秘匿性やそれを実装するワンタイムパッド暗号、完全秘匿性を持つ暗号における鍵の長さに関する定理の証明などを勉強しました。安永さん（東工大の先生ですね）の本を購入し、ま…

今回は完全秘匿性の話題に戻り、シャノンの論文でも証明されている、鍵の集合$K$と平文の集合$M$の大きさに関する定理をLean4で形式化して証明します。 https://tcc.c.titech.ac.jp/yasunaga/appmath6/perfect.pdf では定理６として述べられている次の定理で…

シャノンが暗号に関する論文で「完全秘匿性」という概念を定式化したことを紹介し、そのLean4での形式化までを前回の記事で紹介しました。 この概念がただの抽象概念で、そのような性質を満たす暗号など簡単には作れない、、、という話かというとそうではあ…