この先の議論を展望するために、何のために計算量的安全性の議論をしているのか、今一度振り返ります。シャノンが導入した完全秘匿性にはその暗号文から平文の情報が全く漏れないという素晴らしい性質があります。同時に鍵と平文の長さは同じだけ必要、とか…

意味的安全性と計算量的識別不可能性の定義を再掲し、それぞれのLean4による形式化をみてみます。簡単な方から行くのが良いですよね。まずは定義3.5とその形式化です。 定義3.5 (t, ε)-識別不可能性 共通鍵暗号方式(Enc, Dec)が(t, ε)-識別不可能であるとは…

安永先生の本「暗号理論入門」では第３章で計算量的な安全性を導入します。 ここからは勉強したことのメモとLean4による定義および定理を述べますが、理論の背景は述べません。ぜひ安永先生の本で勉強してください。またLean4による証明も記載しませんが、Gi…

今まで安永先生の「暗号理論入門」第１章、第２章をベースに完全秘匿性を中心とした暗号の安全性について勉強してきました。ここから先はいよいよ計算量的安全性の話に入ります。 完全秘匿性を持つ暗号には「鍵空間のサイズは平文空間のサイズと同じかより大…