proofs/crypto/aead/laws.bend

bend-collections-laws-crypto@1.0.0.0 · 215 lines · 22 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead.bend as A
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as CP
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as RC
5import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as R
6import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as G
7
8# The clauses of the AEAD facade src/crypto/aead.bend (proved in proof.bend,
9# one case per algorithm). hk / hn: the key and nonce have the algorithm's
10# lengths.
11
12# The tag the specification computes over ciphertext ct: decrypt accepts
13# ct || t exactly for this t.
14def expected_tag(alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +ct: List<&2, U32>) -> List<&2, U32>:
15  match alg:
16    case A.CHACHA20_POLY1305{}: R.tag(key, nonce, aad, ct)
17    case A.XCHACHA20_POLY1305{}: R.tag(RC.xsubkey(key, nonce), RC.xnonce(nonce), aad, ct)
18    case A.AES_128_GCM{}: G.aes_tag(key, nonce, aad, ct)
19    case A.AES_256_GCM{}: G.aes_tag(key, nonce, aad, ct)
20
21# decrypt applied to what encrypt returned (None stays None).
22def decrypt_sealed(+alg: A.Alg, +key: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, m: Maybe<&2, List<&2, U32>>) -> Maybe<&2, List<&2, U32>>:
23  match m:
24    case None{}: None{}
25    case Some{c}: A.decrypt(alg, key, nonce, aad, c)
26
27# ---- each algorithm is its specification
28
29law chacha20poly1305.seal:
30  for +key: List<&2, U32>
31  for +nonce: List<&2, U32>
32  for +aad: List<&2, U32>
33  for +pt: List<&2, U32>
34  {A.seal(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
35
36law chacha20poly1305.open:
37  for +key: List<&2, U32>
38  for +nonce: List<&2, U32>
39  for +aad: List<&2, U32>
40  for +data: List<&2, U32>
41  {A.open(A.CHACHA20_POLY1305{}, key, nonce, aad, data) == R.open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
42
43law xchacha20poly1305.seal:
44  for +key: List<&2, U32>
45  for +nonce: List<&2, U32>
46  for +aad: List<&2, U32>
47  for +pt: List<&2, U32>
48  {A.seal(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) == Some{R.xseal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
49
50law xchacha20poly1305.open:
51  for +key: List<&2, U32>
52  for +nonce: List<&2, U32>
53  for +aad: List<&2, U32>
54  for +data: List<&2, U32>
55  {A.open(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) == R.xopen(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
56
57law aes128gcm.seal:
58  for +key: List<&2, U32>
59  for +hk: {List.length(&2, U32, key) == 16n : Nat}
60  for +nonce: List<&2, U32>
61  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
62  for +aad: List<&2, U32>
63  for +pt: List<&2, U32>
64  {A.seal(A.AES_128_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
65
66law aes128gcm.open:
67  for +key: List<&2, U32>
68  for +hk: {List.length(&2, U32, key) == 16n : Nat}
69  for +nonce: List<&2, U32>
70  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
71  for +aad: List<&2, U32>
72  for +data: List<&2, U32>
73  {A.open(A.AES_128_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
74
75law aes256gcm.seal:
76  for +key: List<&2, U32>
77  for +hk: {List.length(&2, U32, key) == 32n : Nat}
78  for +nonce: List<&2, U32>
79  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
80  for +aad: List<&2, U32>
81  for +pt: List<&2, U32>
82  {A.seal(A.AES_256_GCM{}, key, nonce, aad, pt) == Some{G.aes_seal(key, nonce, aad, pt)} : Maybe<&2, List<&2, U32>>}
83
84law aes256gcm.open:
85  for +key: List<&2, U32>
86  for +hk: {List.length(&2, U32, key) == 32n : Nat}
87  for +nonce: List<&2, U32>
88  for +hn: {List.length(&2, U32, nonce) == 12n : Nat}
89  for +aad: List<&2, U32>
90  for +data: List<&2, U32>
91  {A.open(A.AES_256_GCM{}, key, nonce, aad, data) == G.aes_open(key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
92
93# The per-algorithm checked ChaCha20-Poly1305 API agrees with the facade.
94law chacha20poly1305.encrypt:
95  for +key: List<&2, U32>
96  for +nonce: List<&2, U32>
97  for +aad: List<&2, U32>
98  for +pt: List<&2, U32>
99  {CP.encrypt(key, nonce, aad, pt) == A.encrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
100
101law chacha20poly1305.decrypt:
102  for +key: List<&2, U32>
103  for +nonce: List<&2, U32>
104  for +aad: List<&2, U32>
105  for +data: List<&2, U32>
106  {CP.decrypt(key, nonce, aad, data) == A.decrypt(A.CHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
107
108law xchacha20poly1305.encrypt:
109  for +key: List<&2, U32>
110  for +nonce: List<&2, U32>
111  for +aad: List<&2, U32>
112  for +pt: List<&2, U32>
113  {CP.xencrypt(key, nonce, aad, pt) == A.encrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
114
115law xchacha20poly1305.decrypt:
116  for +key: List<&2, U32>
117  for +nonce: List<&2, U32>
118  for +aad: List<&2, U32>
119  for +data: List<&2, U32>
120  {CP.xdecrypt(key, nonce, aad, data) == A.decrypt(A.XCHACHA20_POLY1305{}, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
121
122# ---- the checked API
123
124law encrypt.valid:
125  for +alg: A.Alg
126  for +key: List<&2, U32>
127  for +nonce: List<&2, U32>
128  for +aad: List<&2, U32>
129  for +pt: List<&2, U32>
130  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
131  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
132  {A.encrypt(alg, key, nonce, aad, pt) == A.seal(alg, key, nonce, aad, pt) : Maybe<&2, List<&2, U32>>}
133
134law encrypt.invalid:
135  for +alg: A.Alg
136  for +key: List<&2, U32>
137  for +nonce: List<&2, U32>
138  for +aad: List<&2, U32>
139  for +pt: List<&2, U32>
140  for +h: {A.valid(alg, key, nonce) == False{} : Bool}
141  {A.encrypt(alg, key, nonce, aad, pt) == None{} : Maybe<&2, List<&2, U32>>}
142
143law decrypt.valid:
144  for +alg: A.Alg
145  for +key: List<&2, U32>
146  for +nonce: List<&2, U32>
147  for +aad: List<&2, U32>
148  for +data: List<&2, U32>
149  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
150  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
151  {A.decrypt(alg, key, nonce, aad, data) == A.open(alg, key, nonce, aad, data) : Maybe<&2, List<&2, U32>>}
152
153law decrypt.invalid:
154  for +alg: A.Alg
155  for +key: List<&2, U32>
156  for +nonce: List<&2, U32>
157  for +aad: List<&2, U32>
158  for +data: List<&2, U32>
159  for +h: {A.valid(alg, key, nonce) == False{} : Bool}
160  {A.decrypt(alg, key, nonce, aad, data) == None{} : Maybe<&2, List<&2, U32>>}
161
162# ---- the AEAD properties
163
164# decrypt(encrypt(x)) == Some(x).
165law roundtrip:
166  for +alg: A.Alg
167  for +key: List<&2, U32>
168  for +nonce: List<&2, U32>
169  for +aad: List<&2, U32>
170  for +pt: List<&2, U32>
171  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
172  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
173  {decrypt_sealed(alg, key, nonce, aad, A.encrypt(alg, key, nonce, aad, pt)) == Some{pt} : Maybe<&2, List<&2, U32>>}
174
175# ciphertext || t is rejected for every 16-byte t other than the tag of the
176# ciphertext under this key, nonce and aad.
177law forgery:
178  for +alg: A.Alg
179  for +key: List<&2, U32>
180  for +nonce: List<&2, U32>
181  for +aad: List<&2, U32>
182  for +ct: List<&2, U32>
183  for +t: List<&2, U32>
184  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
185  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
186  for +ht: {List.length(&2, U32, t) == 16n : Nat}
187  for ne: {t != expected_tag(alg, key, nonce, aad, ct) : List<&2, U32>}
188  {A.decrypt(alg, key, nonce, aad, List.append(&2, U32, ct, t)) == None{} : Maybe<&2, List<&2, U32>>}
189
190# What encrypt returns is a ciphertext followed by its expected tag.
191law seal_layout:
192  for +alg: A.Alg
193  for +key: List<&2, U32>
194  for +nonce: List<&2, U32>
195  for +aad: List<&2, U32>
196  for +pt: List<&2, U32>
197  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
198  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
199  exs ct: List<&2, U32>
200  {A.encrypt(alg, key, nonce, aad, pt) == Some{List.append(&2, U32, ct, expected_tag(alg, key, nonce, aad, ct))} : Maybe<&2, List<&2, U32>>}
201
202# Decryption is sound: whatever decrypt accepts is exactly what encrypt
203# produces for the returned plaintext (so every accepted input is the honest
204# ciphertext of its plaintext under this key, nonce and aad).
205law decrypt_sound:
206  for +alg: A.Alg
207  for +key: List<&2, U32>
208  for +nonce: List<&2, U32>
209  for +aad: List<&2, U32>
210  for +data: List<&2, U32>
211  for +p: List<&2, U32>
212  for +hk: {List.length(&2, U32, key) == A.key_size(alg) : Nat}
213  for +hn: {List.length(&2, U32, nonce) == A.nonce_size(alg) : Nat}
214  for +h: {A.decrypt(alg, key, nonce, aad, data) == Some{p} : Maybe<&2, List<&2, U32>>}
215  {A.encrypt(alg, key, nonce, aad, p) == Some{data} : Maybe<&2, List<&2, U32>>}