proofs/crypto/chacha/xchacha.bend
bend-collections-laws-crypto@1.0.0.0 · 71 lines · 6 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as C
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as K
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as T
7
8
9
10
11
12
13def hout(+l: List<&2, U32>) -> List<&2, U32>:
14 R.serialize([R.get(l, 0n), R.get(l, 1n), R.get(l, 2n), R.get(l, 3n), R.get(l, 12n), R.get(l, 13n), R.get(l, 14n), R.get(l, 15n)])
15
16law hbody_correct:
17 for +r: Nat
18 for +kb: List<&2, U32>
19 for +nb: List<&2, U32>
20 {I.hchacha_body(r, kb, nb) == R.hchacha_body(r, kb, nb) : List<&2, U32>}
21
22def hbody_correct(r, kb, nb):
23 +H = I.hstate(I.key_words(I.words(kb)), I.words(nb))
24 Equal.trans(List<&2, U32>, C.hbytes(C.rounds(r, H)), hout(K.vec(C.rounds(r, H))), R.hchacha_body(r, kb, nb),
25 K.hbytes_correct(C.rounds(r, H)),
26 Equal.trans(List<&2, U32>, hout(K.vec(C.rounds(r, H))), hout(R.inner_blocks(r, K.vec(H))), R.hchacha_body(r, kb, nb),
27 Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(l), K.vec(C.rounds(r, H)), R.inner_blocks(r, K.vec(H)), K.rounds_correct(r, H)),
28 Equal.trans(List<&2, U32>, hout(R.inner_blocks(r, K.vec(H))), hout(R.inner_blocks(r, R.hstate(I.words(kb), I.words(nb)))), R.hchacha_body(r, kb, nb),
29 Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, l)), K.vec(H), R.hstate(I.words(kb), I.words(nb)), T.hstate_eq(I.words(kb), I.words(nb))),
30 Equal.trans(List<&2, U32>, hout(R.inner_blocks(r, R.hstate(I.words(kb), I.words(nb)))), hout(R.inner_blocks(r, R.hstate(R.words(kb), I.words(nb)))), R.hchacha_body(r, kb, nb),
31 Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, R.hstate(l, I.words(nb)))), I.words(kb), R.words(kb), T.words_eq(kb)),
32 Equal.cong(List<&2, U32>, List<&2, U32>, l => hout(R.inner_blocks(r, R.hstate(R.words(kb), l))), I.words(nb), R.words(nb), T.words_eq(nb))))))
33
34law hchacha_rounds_correct:
35 for +r: Nat
36 for +kb: List<&2, U32>
37 for +nb: List<&2, U32>
38 {I.hchacha_rounds(r, kb, nb) == R.hchacha_rounds(r, kb, nb) : List<&2, U32>}
39
40def hchacha_rounds_correct(r, kb, nb):
41 match kb:
42 case Nil{}: hbody_correct(r, Nil{}, nb)
43 case b <> rest: hbody_correct(r, b <> rest, nb)
44
45law hchacha20_correct:
46 for +kb: List<&2, U32>
47 for +nb: List<&2, U32>
48 {I.hchacha20_unchecked(kb, nb) == R.hchacha20(kb, nb) : List<&2, U32>}
49
50def hchacha20_correct(kb, nb):
51 hchacha_rounds_correct(10n, kb, nb)
52
53law xencrypt_correct:
54 for +kb: List<&2, U32>
55 for +c: U32
56 for +nb: List<&2, U32>
57 for +pt: List<&2, U32>
58 {I.xencrypt_unchecked(kb, c, nb, pt) == R.xencrypt(kb, c, nb, pt) : List<&2, U32>}
59
60def xenc(+kb: List<&2, U32>, +c: U32, +sub: List<&2, U32>, +nn: List<&2, U32>, +pt: List<&2, U32>) -> List<&2, U32>:
61 R.encrypt_rounds(10n, sub, c, 0 <> 0 <> 0 <> 0 <> nn, pt)
62
63def xencrypt_correct(kb, c, nb, pt):
64 +sub = I.hchacha20_unchecked(kb, I.take(16n, nb))
65 Equal.trans(List<&2, U32>, I.encrypt_rounds(10n, sub, c, 0 <> 0 <> 0 <> 0 <> I.skip(16n, nb), pt), xenc(kb, c, sub, I.skip(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
66 T.encrypt_correct(10n, sub, c, 0 <> 0 <> 0 <> 0 <> I.skip(16n, nb), pt),
67 Equal.trans(List<&2, U32>, xenc(kb, c, sub, I.skip(16n, nb), pt), xenc(kb, c, sub, R.suffix(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
68 Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, sub, l, pt), I.skip(16n, nb), R.suffix(16n, nb), T.skip_eq(16n, nb)),
69 Equal.trans(List<&2, U32>, xenc(kb, c, sub, R.suffix(16n, nb), pt), xenc(kb, c, R.hchacha20(kb, I.take(16n, nb)), R.suffix(16n, nb), pt), R.xencrypt(kb, c, nb, pt),
70 Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, l, R.suffix(16n, nb), pt), sub, R.hchacha20(kb, I.take(16n, nb)), hchacha20_correct(kb, I.take(16n, nb))),
71 Equal.cong(List<&2, U32>, List<&2, U32>, l => xenc(kb, c, R.hchacha20(kb, l), R.suffix(16n, nb), pt), I.take(16n, nb), R.prefix(16n, nb), T.take_eq(16n, nb)))))