~/jendhub

proofs/math/random/chacha8/stream.bend

bend-collections-laws-crypto@1.0.0.0 · 85 lines · 7 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
3import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B
4import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
5import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as S
6import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
7import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend as PB
8
9# The ChaCha8 generator of src/math/random/chacha8.bend produces C2SP's
10# stream (spec/math/random/chacha8rand.bend) for every key: its state (key,
11# next group, unread words of the current group) stands for the words left
12# of the current iteration and the key of the next one.
13
14def app(xs: List<&2, W.U64>, ys: List<&2, W.U64>) -> List<&2, W.U64>:
15  match xs:
16    case Nil{}:
17      ys
18    case Con{x, rest}:
19      Con{x, app(rest, ys)}
20
21def drop64(n: Nat, xs: List<&2, W.U64>) -> List<&2, W.U64>:
22  match n xs:
23    case 0n _:
24      xs
25    case 1n+p Nil{}:
26      []
27    case 1n+p Con{x, rest}:
28      drop64(p, rest)
29
30# the outputs of the current iteration after the groups already produced
31def rest(+kl: List<&2, U32>, p: C8.Phase) -> List<&2, W.U64>:
32  match p:
33    case C8.G0{}:
34      []
35    case C8.G1{}:
36      drop64(32n, S.words64(S.output(kl)))
37    case C8.G2{}:
38      drop64(64n, S.words64(S.output(kl)))
39    case C8.G3{}:
40      drop64(96n, S.words64(S.output(kl)))
41
42# the key of the iteration after them
43def nk(+kl: List<&2, U32>, p: C8.Phase) -> List<&2, U32>:
44  match p:
45    case C8.G0{}:
46      kl
47    case C8.G1{}:
48      S.next_key(kl)
49    case C8.G2{}:
50      S.next_key(kl)
51    case C8.G3{}:
52      S.next_key(kl)
53
54def gw(+k: B.Key, +c: U32) -> List<&2, W.U64>:
55  S.words64(S.group(S.key_list(k), c))
56
57# the invariant: from state C{k, p, buf} the generator outputs buf, the rest
58# of the iteration keyed by k, then C2SP's stream from the next key
59def inv(+n: Nat, +k: B.Key, +buf: List<&2, W.U64>, +p: C8.Phase) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.C{k, p, buf}) == S.stream_go(n, app(buf, rest(S.key_list(k), p)), nk(S.key_list(k), p)) : List<&2, W.U64>}:
60  match n:
61    case 0n:
62      {==}
63    case 1n+m:
64      match buf:
65        case Con{x, t}:
66          Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{x, l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, p, t}), S.stream_go(m, app(t, rest(S.key_list(k), p)), nk(S.key_list(k), p)), inv(m, k, t, p))
67        case Nil{}:
68          match p:
69            case C8.G0{}:
70              %Equal.sym(List<&2, W.U64>, B.group(k, 0), gw(k, 0), PB.group_correct(k, 0)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})))} == S.stream_go(1n+m, [], S.key_list(k)) : List<&2, W.U64>}
71              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 0)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G1{}, S.tail(gw(k, 0))}), S.stream_go(m, app(S.tail(gw(k, 0)), rest(S.key_list(k), C8.G1{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 0)), C8.G1{}))
72            case C8.G1{}:
73              %Equal.sym(List<&2, W.U64>, B.group(k, 4), gw(k, 4), PB.group_correct(k, 4)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G1{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
74              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 4)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G2{}, S.tail(gw(k, 4))}), S.stream_go(m, app(S.tail(gw(k, 4)), rest(S.key_list(k), C8.G2{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 4)), C8.G2{}))
75            case C8.G2{}:
76              %Equal.sym(List<&2, W.U64>, B.group(k, 8), gw(k, 8), PB.group_correct(k, 8)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G2{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
77              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 8)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G3{}, S.tail(gw(k, 8))}), S.stream_go(m, app(S.tail(gw(k, 8)), rest(S.key_list(k), C8.G3{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 8)), C8.G3{}))
78            case C8.G3{}:
79              %Equal.sym(List<&2, W.U64>, B.group(k, 12), gw(k, 12), PB.group_correct(k, 12)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.last(_))), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.last(_))))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G3{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
80              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 12)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), C8.G0{}, S.tail(List.take(&2, W.U64, gw(k, 12), 28n))}), S.stream_go(m, app(S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), []), S.key_list(C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)))), inv(m, C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), C8.G0{}))
81
82# THEOREM: the generator keyed by k outputs C2SP's ChaCha8Rand stream keyed
83# by k's eight words, for every key and every number of outputs
84def stream(+n: Nat, +k: B.Key) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.of_key(k)) == S.stream(n, S.key_list(k)) : List<&2, W.U64>}:
85  inv(n, k, [], C8.G0{})