security gameのclassifying topoi
## Trigger
暗号学的 hash を、理想的な単射や random oracle そのものではなく、現実の有限状態 implementation と有限時間 adversary の相互作用として geometric/coherent theory に書きたいという議論から。
## Idea
まず有限の resource bounds を固定する。典型的には
- 最大 message length $L$
- digest length $d$
- hash state size $s$
- implementation code size $S$
- adversary running time $T$
- query bound $Q$
- random tape length $R$
- 許容 winning tapes 数 $K$
である。
この固定された tuple $b=(L,d,s,S,T,Q,R,K)$ に対し、有限 register machine / circuit として hash implementation を記述する coherent theory $\mathbb T_{\mathrm{impl},b}$ を作る。Set-model は、指定された有限 resource bound を満たす具体的な hash program である。
adversary の bounded small-step execution relation $\operatorname{Exec}_{T,Q}$ と、collision を表す positive formula $\operatorname{Win}_{\mathrm{coll}}(a,r)$ を追加する。random tape は有限集合 $\mathsf{Bit}^R$ なので、確率上界は実数や measure を導入せず、次の finite-cardinality sequent で表現できる：
\[
\bigwedge_{j=0}^{K}\operatorname{Win}_{\mathrm{coll}}(a,r_j)
\;\vdash\;
\bigvee_{0\leq i<j\leq K} r_i=r_j.
\]
これは各 adversary $a$ に対し winning random tapes が高々 $K$ 個であること、したがって一様 random tape に関する成功確率が高々 $K/2^R$ であることを意味する。
implementation 全体を classify する topos を
\[
\mathcal E_{\mathrm{impl},b}:=\mathbf{Set}[\mathbb T_{\mathrm{impl},b}]
\]
とし、上の security axiom を加えた quotient theory の classifying topos を
\[
\mathcal E_{\mathrm{CR},b}\hookrightarrow \mathcal E_{\mathrm{impl},b}
\]
とする。具体的 implementation $H$ が bound $b$ に対して collision resistant であることは、その point
\[
p_H:\mathbf{Set}\to\mathcal E_{\mathrm{impl},b}
\]
が security subtopos $\mathcal E_{\mathrm{CR},b}$ を経由して factorize することとして表される。
resource bounds を変化させると、$\mathbb N^m$ または resource-bound poset で添字づけられた topoi/subtopoi の diagram が得られる。より強い attacker やより厳しい failure bound に対して security subtopos は小さくなる。したがって hash implementation の security profile を、どの bounds に対して factorization が成立するかという categorical invariant として定義できる。
## Goal
暗号学的 security を「性質を満たす関数」ではなく、「有限の security game に勝てる adversary の数・random tapes の数」という operational data から classifying topos の quotient/subtopos として再構成する。correctness test vectors、preimage resistance、second-preimage resistance も別々の quotient theory として扱い、それらの meet によって verified-and-secure implementations の moduli topos を得たい。
## Personal context
洞の昔の戦略の圏では、入力語の自由対象 $\Lambda^*$ から状態機械 $X$ への一意な射と output map $X\to H$ の合成で behavior を表した。この構図を streaming hash machine に再利用できる。さらに、洞の quotient topos / subtopos の研究と、security property を quotient theory として課す構図が直接接続する。