proof/AES_NistTagProof.bend
qasim-bend-kit@0.1.0.2 · 76 lines · 8 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
3import qasim-bend-kit@0.1.0.2/proof/AES_NistKeyScheduleProof.bend as Key
4import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockProof.bend as J0
5import qasim-bend-kit@0.1.0.2/proof/AES_NistBlockComposeProof.bend as J0Proof
6import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockProof.bend as Hash
7import qasim-bend-kit@0.1.0.2/proof/AES_NistHashBlockComposeProof.bend as HashProof
8
9def zero() -> List<&2, U32>:
10 [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]
11
12def auth_from_hash(+h: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>) -> List<&2, U32>:
13 Core.ghash_auth_with_hash(h, aad, bytes)
14
15def tag_from_parts(auth: List<&2, U32>, mask: List<&2, U32>) -> List<&2, U32>:
16 Core.gcm_mask_bytes(Core.gcm_tag_parts(auth, mask))
17
18def tag_shape(+words: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>) ->
19 {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) ==
20 tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))) : List<&2, U32>}:
21 match nonce:
22 case Nil{}: {==}
23 case head <> tail: {==}
24
25def auth_from_checked_hash(+words: List<&2, U32>, +h: List<&2, U32>,
26 +aad: List<&2, U32>, +bytes: List<&2, U32>, +auth: List<&2, U32>,
27 hash_matches: {Core.aes256_encrypt_expanded(words, [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]) == h : List<&2, U32>},
28 computed: {auth_from_hash(h, aad, bytes) == auth : List<&2, U32>}) ->
29 {Core.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>}:
30 Equal.trans(List<&2, U32>,
31 Core.ghash_auth_expanded(words, aad, bytes),
32 auth_from_hash(h, aad, bytes), auth,
33 Equal.cong(List<&2, U32>, List<&2, U32>, h => auth_from_hash(h, aad, bytes),
34 Core.aes256_encrypt_expanded(words, [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]), h, hash_matches),
35 computed)
36
37def aes_block_input_matches(+words: List<&2, U32>, +input: List<&2, U32>, +block: List<&2, U32>, +result: List<&2, U32>,
38 input_matches: {input == block : List<&2, U32>},
39 block_matches: {Core.aes256_encrypt_expanded(words, block) == result : List<&2, U32>}) ->
40 {Core.aes256_encrypt_expanded(words, input) == result : List<&2, U32>}:
41 Equal.trans(List<&2, U32>, Core.aes256_encrypt_expanded(words, input),
42 Core.aes256_encrypt_expanded(words, block), result,
43 Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.aes256_encrypt_expanded(words, value),
44 input, block, input_matches), block_matches)
45
46def finish_tag(+words: List<&2, U32>, +nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>,
47 +auth: List<&2, U32>, +mask: List<&2, U32>, +tag: List<&2, U32>,
48 auth_matches: {Core.ghash_auth_expanded(words, aad, bytes) == auth : List<&2, U32>},
49 mask_matches: {Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce)) == mask : List<&2, U32>},
50 xor_matches: {tag_from_parts(auth, mask) == tag : List<&2, U32>}) ->
51 {Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)) == tag : List<&2, U32>}:
52 Equal.trans(List<&2, U32>, Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, bytes)),
53 tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))), tag,
54 tag_shape(words, nonce, aad, bytes),
55 Equal.trans(List<&2, U32>,
56 tag_from_parts(Core.ghash_auth_expanded(words, aad, bytes), Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
57 tag_from_parts(auth, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))), tag,
58 Equal.cong(List<&2, U32>, List<&2, U32>, value => tag_from_parts(value, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
59 Core.ghash_auth_expanded(words, aad, bytes), auth, auth_matches),
60 Equal.trans(List<&2, U32>, tag_from_parts(auth, Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce))),
61 tag_from_parts(auth, mask), tag,
62 Equal.cong(List<&2, U32>, List<&2, U32>, value => tag_from_parts(auth, value),
63 Core.aes256_encrypt_expanded(words, Core.gcm_j0(nonce)), mask, mask_matches), xor_matches)))
64
65def nist_tag(+nonce: List<&2, U32>, +aad: List<&2, U32>, +bytes: List<&2, U32>,
66 +auth: List<&2, U32>, +tag: List<&2, U32>,
67 j0_matches: {Core.gcm_j0(nonce) == J0.block() : List<&2, U32>},
68 auth_matches: {auth_from_hash(Hash.result(), aad, bytes) == auth : List<&2, U32>},
69 xor_matches: {tag_from_parts(auth, J0.result()) == tag : List<&2, U32>}) ->
70 {Core.gcm_tag_bytes(Core.gcm_tag_output(Key.words_60(), nonce, aad, bytes)) == tag : List<&2, U32>}:
71 finish_tag(Key.words_60(), nonce, aad, bytes, auth, J0.result(), tag,
72 auth_from_checked_hash(Key.words_60(), Hash.result(), aad, bytes, auth,
73 aes_block_input_matches(Key.words_60(), [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], Hash.block(), Hash.result(),
74 {==}, HashProof.expanded_block_matches()), auth_matches),
75 aes_block_input_matches(Key.words_60(), Core.gcm_j0(nonce), J0.block(), J0.result(),
76 j0_matches, J0Proof.expanded_block_matches()), xor_matches)