proof/AES_CoreTagProof.bend
qasim-bend-kit@0.1.0.2 · 117 lines · 13 definitions
1import Base
2import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
3import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core
4
5def output_ciphertext(output: Core.GcmOutput) -> List<&2, U32>:
6 match output:
7 case Core.GcmOutput{ciphertext, ciphertext_valid,
8 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
9 tag_matches}:
10 ciphertext
11
12def output_tag(output: Core.GcmOutput) -> List<&2, U32>:
13 match output:
14 case Core.GcmOutput{ciphertext, ciphertext_valid,
15 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
16 tag_matches}:
17 tag_bytes
18
19def output_tag_words(output: Core.GcmOutput) -> List<&2, U32>:
20 match output:
21 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
22 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
23 tag_words
24
25def output_tag_nonce(output: Core.GcmOutput) -> List<&2, U32>:
26 match output:
27 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
28 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
29 tag_nonce
30
31def output_tag_aad(output: Core.GcmOutput) -> List<&2, U32>:
32 match output:
33 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
34 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
35 tag_aad
36
37def output_tag_ciphertext(output: Core.GcmOutput) -> List<&2, U32>:
38 match output:
39 case Core.GcmOutput{ciphertext, ciphertext_valid, tag_bytes,
40 tag_valid, tag_size, tag_words, tag_nonce, tag_aad, tag_matches}:
41 ciphertext
42
43def output_from_ciphertext_matches(+words: List<&2, U32>,
44 +nonce: List<&2, U32>, +aad: List<&2, U32>,
45 +cipher_output: Core.GcmCiphertext) ->
46 {output_ciphertext(Core.gcm_output_from_ciphertext(words, nonce, aad,
47 cipher_output)) == Core.gcm_ciphertext_bytes(cipher_output) :
48 List<&2, U32>}:
49 match cipher_output:
50 case Core.GcmCiphertext{bytes, valid}: {==}
51
52
53
54def output_ciphertext_valid(+output: Core.GcmOutput) ->
55 {Core.gcm_bytes_valid(output_ciphertext(output)) == True{} : Bool}:
56 match output:
57 case Core.GcmOutput{ciphertext, ciphertext_valid,
58 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
59 tag_matches}:
60 ciphertext_valid
61
62def output_tag_valid(+output: Core.GcmOutput) ->
63 {Core.gcm_bytes_valid(output_tag(output)) == True{} : Bool}:
64 match output:
65 case Core.GcmOutput{ciphertext, ciphertext_valid,
66 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
67 tag_matches}:
68 tag_valid
69
70def envelope_gcm_ciphertext(nonce: AES.Nonce,
71 output: Core.GcmOutput) ->
72 {AES.ciphertext(AES.envelope_from_gcm_checked(nonce, output)) ==
73 output_ciphertext(output) : List<&2, U32>}:
74 match output:
75 case Core.GcmOutput{ciphertext, ciphertext_valid,
76 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
77 tag_matches}: {==}
78
79def envelope_gcm_tag(nonce: AES.Nonce,
80 output: Core.GcmOutput) ->
81 {AES.tag_bytes(AES.envelope_tag(
82 AES.envelope_from_gcm_checked(nonce, output))) ==
83 output_tag(output) : List<&2, U32>}:
84 match output:
85 case Core.GcmOutput{ciphertext, ciphertext_valid,
86 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
87 tag_matches}: {==}
88
89def envelope_gcm_nonce(nonce: AES.Nonce,
90 output: Core.GcmOutput) ->
91 {AES.raw_nonce_bytes(AES.envelope_nonce(
92 AES.envelope_from_gcm_checked(nonce, output))) ==
93 AES.raw_nonce_bytes(nonce) : List<&2, U32>}:
94 match output:
95 case Core.GcmOutput{ciphertext, ciphertext_valid,
96 tag_bytes, tag_valid, tag_size, tag_words, tag_nonce, tag_aad,
97 tag_matches}: {==}
98
99def raw_encrypt_output_ciphertext(+key: List<&2, U32>,
100 +nonce: List<&2, U32>, +aad: List<&2, U32>,
101 +plaintext: List<&2, U32>) ->
102 {output_ciphertext(Core.gcm_encrypt_raw(key, nonce, aad, plaintext)) ==
103 Core.gcm_zip_xor(plaintext,
104 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
105 Core.aes256_expand(key),
106 Core.gcm_inc32(Core.gcm_j0(nonce)))) : List<&2, U32>}:
107 Equal.trans(List<&2, U32>,
108 output_ciphertext(Core.gcm_encrypt_raw(key, nonce, aad, plaintext)),
109 Core.gcm_ciphertext_bytes(Core.gcm_ctr_encrypt(
110 Core.aes256_expand(key), nonce, plaintext)),
111 Core.gcm_zip_xor(plaintext,
112 Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
113 Core.aes256_expand(key),
114 Core.gcm_inc32(Core.gcm_j0(nonce)))),
115 output_from_ciphertext_matches(Core.aes256_expand(key), nonce, aad,
116 Core.gcm_ctr_encrypt(Core.aes256_expand(key), nonce, plaintext)),
117 {==})