完全秘匿性、同値な命題とLean4での形式化

完全秘匿性という概念、せっかく数学的に定義したのですが数式が出てこないと数学している気分になれません。というわけで暗号の完全秘匿性について数式を用いて定義してみましょう。また数式化できればLean4での形式化も見たいですよね。とは言っても暗号というものを定義するために流石に少し準備が必要です。 平文(メ…