前回はネクストビット予測不可能性から擬似ランダムであることを導く定理4.2のLean4による証明を解説しました。その記事の最後にBitVecとその依存型の面倒臭さについて言及しました。 Lean4は関数型言語で依存型もサポートしていて数学の証明にも使える！み…

前回に続いてネクストビット予測不可能性の話です。今回は前回の定理の逆、つまりネクストビット予測不可能性から擬似ランダムを示します。 安永さんの著書： 暗号理論入門 作者:安永 憲司 森北出版 Amazon では定理4.2 としてその証明まで掲載されています…

PRG（擬似ランダム生成器）ならネクストビット予測不可能性が成り立つを示すのはよくよく考えると当然！のような気がしてきます！ まずPRGが生成する数（ビット列）の分布は一様分布と計算量的に見分けがつきません。ここから（おそらく）PRGが生成した数（…

前の一連の記事では擬似乱数や擬似乱数生成器を定義し、その数学的な性質を証明してきました。その際には確率分布の計算量的識別不可能性などを利用しました。擬似乱数とは一様分布と計算量的に識別不可能な確率分布のことでした。 これからしばらくネクスト…

擬似乱数を1bit伸ばすことができれば、任意の長さの擬似乱数に伸ばすことができます。この定理をLean4で形式化しました。 定理4.1 擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$に対し、$G':\{0,1\}^n \rightarrow\{0,1\}^L$を「 $x_0 = x, i=0,…

n bitの一様乱数を入力としてn+1 bitの擬似乱数をつくる擬似乱数生成器$G : \{0,1\}^n \rightarrow \{0,1\}^{n+1}$があるとします。Gを組み合わせることによって任意のL (L ≧ 1) bitまで擬似乱数を伸ばすことができます。具体的にはn bitの一様乱数を入力と…

まずはなにあれ、一様分布を定義しましょう。一様分布$U_n$とは長さnの全てのビット列の集合$\{0,1\}^n$の各要素について確率$\frac{1}{2^n}$を割り当てた分布として定義します。集合$\{0,1\}^n$の要素の数は$2^n$ですからすべての要素に確率を均等に割り当…

「与えられた２つの確率分布を(計算量的に)識別出来ない」という概念を数学的に定義します。 安永先生著： 暗号理論入門 作者:安永 憲司 森北出版 Amazon をお持ちの方はp40, 第４章「擬似ランダム」の冒頭部分を参考にしてください。以下の定義は同書からの…

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

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

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

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

本記事の内容は安永憲司著『暗号理論入門』（森北出版）第2章に基づいています。 前回の記事 では完全模倣性を紹介しました。完全秘匿な暗号では、攻撃者Aは暗号文cを受け取って一生懸命計算しても、暗号文を知らないシミュレータSに完全に真似されてしまい…

攻撃者の視点を導入すると今までとは少し毛色の変わった形で完全秘匿性と同値な命題を定式化することができます。それは模倣性(simulatability)という考えです。 攻撃者Aは暗号文を見て何かを出力する確率的アルゴリズムだとします。その動作は出力の確率分…

今まで議論してきたシャノンの完全秘匿性や識別不可性に基づく完全秘匿性では、「確率が変わらないのだから新たな情報は得られていない」とか「確率分布が変わらないのだから新たな情報は得られていない」ということを数式で定式化して同値性を証明してきま…

シャノンの完全秘匿性による暗号理論を勉強して、定義の形式化およびそれに基づく定理の形式証明をやってきました。それらの記事は、 から始まる一連の記事でした。せっかくなのでこれらの成果を一つのレポジトリにまとめ直して少しでもわかりやすいものにし…

Lean言語・形式証明系の普及を進めておられる北窓さんが執筆された本： ゼロから始めるLean言語入門 ― 手を動かして学ぶ形式数学ライブラリ開発 を購入して読み進めています。 扱っている言語はLean4です。Lean4は多くの数学者にも使われ始めているのですが…

Lean4+Mathlib4の組み合わせで証明が出来上がるとレポジトリをGithubで公開したくなります。この時にGithub Actionsを使ってCI (Continuous Integration)を設定しておくと、利用者がレポジトリをダウンロードしてから利用を開始する体験を向上できます。この…

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

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

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

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

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

これから数回にわたって「セキュリティを数学的に証明する」話を書いていきます。自分の勉強のための覚書みたいなものですし、まだ勉強を始めたばかりの分野なので記載に間違いがあるかもしれません。そもそも理解の方向性が間違っているかもしれません。決…

今日はちょっと別件でネット検索していたらびっくりすることに気がつきました。 テレンスタオ教授（フィールズ賞受賞者、UCLA）が２週間ほど前からユーチューブを始めていて、3本の動画を投稿されています。全部、Lean4の使い方ビデオでした。 www.youtube.c…

前回はコインを2回投げる試行のPMF（確率質量関数）による記述方法を紹介し、2回とも同じ面がでる確率事象の記述の仕方と確率を証明しました。 今回は同じように2回投げる試行で2回とも表が出る確率事象の記述を行い、その確率が1/4であることを証明します。…

前回の記事ではLean4での離散確率の形式化としてPMF (Probability Mass Function, 確率質量関数)について紹介し、コイントスをPMFで記述して、表や裏が出る確率が1/2であることを証明しました。 今回はコインを2回投げる試行のPMFによる記述方法を紹介し、い…

少し事情があって?Lean4での確率の取り扱いについて勉強をしています。とは言っても決して本格的な確率論(測度論をベースにした確率密度関数や確率分布など)ではなく、算数や中学校で習うレベルの確率の話です。いわゆるコイントスの確率やサイコロの確率な…

Mathematics in Leanを読んできましたが、今回を最終回とします。11.1. Elementary Differential Calculusと12.1. Elementary Integrationの内容の紹介です。 import Mathlib open Real-- サイン関数を微分するとコサイン関数example : deriv sin = cos := b…

今日は3月14日、毎年恒例の円周率の日です。 今年はなんと満月なんです。今、まだ今夜の満月を見ていない人、すぐに外に出てください。関東地方は晴れていて見られます。 記念に今夜のお月様を撮って見ました。次に円周率の日に満月が見られるのはいつのこと…