proofs/crypto/chacha/proof.bend
bend-collections-laws-crypto@1.0.0.0 · 134 lines · 4 definitions
1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as I
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as R
4import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws.bend as Laws
5import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as T
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/xchacha.bend as X
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as V
8
9
10
11
12
13
14def Laws.block_rounds(r, key, counter, nonce):
15 T.block_rounds_correct(r, key, counter, nonce)
16
17def Laws.encrypt_rounds(r, key, counter, nonce, plaintext):
18 T.encrypt_correct(r, key, counter, nonce, plaintext)
19
20def Laws.hchacha_rounds(r, key, nonce):
21 X.hchacha_rounds_correct(r, key, nonce)
22
23def Laws.hchacha20(key, nonce):
24 X.hchacha20_correct(key, nonce)
25
26def Laws.xencrypt(key, counter, nonce, plaintext):
27 X.xencrypt_correct(key, counter, nonce, plaintext)
28
29
30
31law when_true:
32 for +ok: Bool
33 for +x: List<&2, U32>
34 for +h: {ok == True{} : Bool}
35 {I.when(ok, x) == Some{x} : Maybe<&2, List<&2, U32>>}
36
37def when_true(ok, x, h):
38 %Equal.sym(Bool, ok, True{}, h) : {I.when(_, x) == Some{x} : Maybe<&2, List<&2, U32>>}
39 {==}
40
41law when_false:
42 for +ok: Bool
43 for +x: List<&2, U32>
44 for +h: {ok == False{} : Bool}
45 {I.when(ok, x) == None{} : Maybe<&2, List<&2, U32>>}
46
47def when_false(ok, x, h):
48 %Equal.sym(Bool, ok, False{}, h) : {I.when(_, x) == None{} : Maybe<&2, List<&2, U32>>}
49 {==}
50
51law valid_true:
52 for +key: List<&2, U32>
53 for +nonce: List<&2, U32>
54 for +n: Nat
55 for +hk: {List.length(&2, U32, key) == 32n : Nat}
56 for +hn: {List.length(&2, U32, nonce) == n : Nat}
57 {I.valid(key, nonce, n) == True{} : Bool}
58
59def is_eq_self(+n: Nat) -> {Nat.is_eq(n, n) == True{} : Bool}:
60 match n:
61 case 0n: {==}
62 case 1n+p: is_eq_self(p)
63
64def valid_true(key, nonce, n, hk, hn):
65 %Equal.sym(Nat, List.length(&2, U32, key), 32n, hk) :
66 {Bool.and(Nat.is_eq(_, 32n), Nat.is_eq(List.length(&2, U32, nonce), n)) == True{} : Bool}
67 %Equal.sym(Nat, List.length(&2, U32, nonce), n, hn) :
68 {Bool.and(Nat.is_eq(32n, 32n), Nat.is_eq(_, n)) == True{} : Bool}
69 is_eq_self(n)
70
71def Laws.chacha20_block.valid(key, counter, nonce, hk, hn):
72 Equal.trans(Maybe<&2, List<&2, U32>>, I.chacha20_block(key, counter, nonce), Some{I.block_rounds(10n, key, counter, nonce)}, Some{R.block(key, counter, nonce)},
73 when_true(I.valid(key, nonce, 12n), I.block_rounds(10n, key, counter, nonce), valid_true(key, nonce, 12n, hk, hn)),
74 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.block_rounds(10n, key, counter, nonce), R.block(key, counter, nonce), T.block_rounds_correct(10n, key, counter, nonce)))
75
76def Laws.chacha20_block.invalid(key, counter, nonce, h):
77 when_false(I.valid(key, nonce, 12n), I.block_rounds(10n, key, counter, nonce), h)
78
79def Laws.chacha20.valid(key, counter, nonce, plaintext, hk, hn):
80 Equal.trans(Maybe<&2, List<&2, U32>>, I.chacha20(key, counter, nonce, plaintext), Some{I.encrypt_rounds(10n, key, counter, nonce, plaintext)}, Some{R.encrypt(key, counter, nonce, plaintext)},
81 when_true(I.valid(key, nonce, 12n), I.encrypt_rounds(10n, key, counter, nonce, plaintext), valid_true(key, nonce, 12n, hk, hn)),
82 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.encrypt_rounds(10n, key, counter, nonce, plaintext), R.encrypt(key, counter, nonce, plaintext), T.encrypt_correct(10n, key, counter, nonce, plaintext)))
83
84def Laws.chacha20.invalid(key, counter, nonce, plaintext, h):
85 when_false(I.valid(key, nonce, 12n), I.encrypt_rounds(10n, key, counter, nonce, plaintext), h)
86
87def Laws.hchacha20.valid(key, nonce, hk, hn):
88 Equal.trans(Maybe<&2, List<&2, U32>>, I.hchacha20(key, nonce), Some{I.hchacha20_unchecked(key, nonce)}, Some{R.hchacha20(key, nonce)},
89 when_true(I.valid(key, nonce, 16n), I.hchacha20_unchecked(key, nonce), valid_true(key, nonce, 16n, hk, hn)),
90 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.hchacha20_unchecked(key, nonce), R.hchacha20(key, nonce), X.hchacha20_correct(key, nonce)))
91
92def Laws.hchacha20.invalid(key, nonce, h):
93 when_false(I.valid(key, nonce, 16n), I.hchacha20_unchecked(key, nonce), h)
94
95def Laws.xchacha20.valid(key, counter, nonce, plaintext, hk, hn):
96 Equal.trans(Maybe<&2, List<&2, U32>>, I.xchacha20(key, counter, nonce, plaintext), Some{I.xencrypt_unchecked(key, counter, nonce, plaintext)}, Some{R.xencrypt(key, counter, nonce, plaintext)},
97 when_true(I.valid(key, nonce, 24n), I.xencrypt_unchecked(key, counter, nonce, plaintext), valid_true(key, nonce, 24n, hk, hn)),
98 Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, l => Some{l}, I.xencrypt_unchecked(key, counter, nonce, plaintext), R.xencrypt(key, counter, nonce, plaintext), X.xencrypt_correct(key, counter, nonce, plaintext)))
99
100def Laws.xchacha20.invalid(key, counter, nonce, plaintext, h):
101 when_false(I.valid(key, nonce, 24n), I.xencrypt_unchecked(key, counter, nonce, plaintext), h)
102
103
104
105def Laws.involution(r, key, counter, nonce, plaintext):
106 +ct = I.encrypt_rounds(r, key, counter, nonce, plaintext)
107 +sct = R.encrypt_rounds(r, key, counter, nonce, plaintext)
108 Equal.trans(List<&2, U32>, I.encrypt_rounds(r, key, counter, nonce, ct), R.encrypt_rounds(r, key, counter, nonce, ct), plaintext,
109 T.encrypt_correct(r, key, counter, nonce, ct),
110 Equal.trans(List<&2, U32>, R.encrypt_rounds(r, key, counter, nonce, ct), R.encrypt_rounds(r, key, counter, nonce, sct), plaintext,
111 Equal.cong(List<&2, U32>, List<&2, U32>, l => R.encrypt_rounds(r, key, counter, nonce, l), ct, sct, T.encrypt_correct(r, key, counter, nonce, plaintext)),
112 V.involution(r, key, counter, nonce, plaintext)))
113
114def Laws.xinvolution(key, counter, nonce, plaintext):
115 +ct = I.xencrypt_unchecked(key, counter, nonce, plaintext)
116 +sct = R.xencrypt(key, counter, nonce, plaintext)
117 Equal.trans(List<&2, U32>, I.xencrypt_unchecked(key, counter, nonce, ct), R.xencrypt(key, counter, nonce, ct), plaintext,
118 X.xencrypt_correct(key, counter, nonce, ct),
119 Equal.trans(List<&2, U32>, R.xencrypt(key, counter, nonce, ct), R.xencrypt(key, counter, nonce, sct), plaintext,
120 Equal.cong(List<&2, U32>, List<&2, U32>, l => R.xencrypt(key, counter, nonce, l), ct, sct, X.xencrypt_correct(key, counter, nonce, plaintext)),
121 V.involution(10n, R.xsubkey(key, nonce), counter, R.xnonce(nonce), plaintext)))
122
123def Laws.encrypt_length(r, key, counter, nonce, plaintext):
124 %Equal.sym(List<&2, U32>, I.encrypt_rounds(r, key, counter, nonce, plaintext), R.encrypt_rounds(r, key, counter, nonce, plaintext), T.encrypt_correct(r, key, counter, nonce, plaintext)) :
125 {List.length(&2, U32, _) == List.length(&2, U32, plaintext) : Nat}
126 V.encrypt_length(r, key, counter, nonce, plaintext)
127
128def Laws.block_length(r, key, counter, nonce):
129 T.block_length(r, key, counter, nonce)
130
131def Laws.hchacha_length(r, key, nonce):
132 match key:
133 case Nil{}: {==}
134 case b <> rest: {==}