proof/AES_KnownAnswerProof.bend
qasim-bend-kit@0.1.0.2 · 136 lines · 4 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
4import qasim-bend-kit@0.1.0.2/proof/AES_CoreTagProof.bend as Fields
5import qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend as Certificate
6
7def tag_equal(+bytes: List<&2, U32>,
8 +size: {List.length(&2, U32, bytes) == 16n : Nat},
9 +valid: {AES.bytes_valid(bytes) == True{} : Bool},
10 +expected: List<&2, U32>, same: {bytes == expected : List<&2, U32>}) ->
11 @+expected_size: {List.length(&2, U32, expected) == 16n : Nat} ->
12 @+expected_valid: {AES.bytes_valid(expected) == True{} : Bool} ->
13 {AES.Tag{bytes, size, valid} ==
14 AES.Tag{expected, expected_size, expected_valid} : AES.Tag}:
15 %same :
16 @+expected_size: {List.length(&2, U32, _) == 16n : Nat} ->
17 @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
18 {AES.Tag{bytes, size, valid} ==
19 AES.Tag{_, expected_size, expected_valid} : AES.Tag}
20 expected_size => expected_valid =>
21 Equal.trans(AES.Tag, AES.Tag{bytes, size, valid},
22 AES.Tag{bytes, expected_size, valid},
23 AES.Tag{bytes, expected_size, expected_valid},
24 Equal.cong({List.length(&2, U32, bytes) == 16n : Nat}, AES.Tag,
25 proof => AES.Tag{bytes, proof, valid}, size, expected_size,
26 Certificate.nat_unique(List.length(&2, U32, bytes), 16n,
27 size, expected_size)),
28 Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.Tag,
29 proof => AES.Tag{bytes, expected_size, proof}, valid,
30 expected_valid, Certificate.bool_unique(AES.bytes_valid(bytes),
31 True{}, valid, expected_valid)))
32
33def envelope_equal(+nonce: AES.Nonce, +ciphertext: List<&2, U32>,
34 +tag: AES.Tag, +valid: {AES.bytes_valid(ciphertext) == True{} : Bool},
35 +expected_ciphertext: List<&2, U32>, +expected_tag: AES.Tag,
36 same_ciphertext: {ciphertext == expected_ciphertext : List<&2, U32>},
37 same_tag: {tag == expected_tag : AES.Tag}) ->
38 @+expected_valid: {AES.bytes_valid(expected_ciphertext) == True{} : Bool} ->
39 {AES.Envelope{nonce, ciphertext, tag, valid} ==
40 AES.Envelope{nonce, expected_ciphertext, expected_tag, expected_valid} :
41 AES.Envelope}:
42 %same_ciphertext :
43 @+expected_valid: {AES.bytes_valid(_) == True{} : Bool} ->
44 {AES.Envelope{nonce, ciphertext, tag, valid} ==
45 AES.Envelope{nonce, _, expected_tag, expected_valid} : AES.Envelope}
46 expected_valid =>
47 Equal.trans(AES.Envelope,
48 AES.Envelope{nonce, ciphertext, tag, valid},
49 AES.Envelope{nonce, ciphertext, expected_tag, valid},
50 AES.Envelope{nonce, ciphertext, expected_tag, expected_valid},
51 Equal.cong(AES.Tag, AES.Envelope,
52 value => AES.Envelope{nonce, ciphertext, value, valid},
53 tag, expected_tag, same_tag),
54 Equal.cong({AES.bytes_valid(ciphertext) == True{} : Bool},
55 AES.Envelope,
56 proof => AES.Envelope{nonce, ciphertext, expected_tag, proof},
57 valid, expected_valid,
58 Certificate.bool_unique(AES.bytes_valid(ciphertext), True{},
59 valid, expected_valid)))
60
61def output_matches(+nonce: AES.Nonce, +output: Core.GcmOutput,
62 +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
63 ciphertext_matches: {Fields.output_ciphertext(output) == ciphertext :
64 List<&2, U32>},
65 tag_matches: {Fields.output_tag(output) == tag_bytes : List<&2, U32>}) ->
66 @+tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat} ->
67 @+tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool} ->
68 @+ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool} ->
69 {AES.encrypt_output_from_gcm(nonce, output) ==
70 Done{AES.Envelope{nonce, ciphertext,
71 AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
72 Result<&2, &2, AES.Error, AES.Envelope>}:
73 match output:
74 case Core.GcmOutput{+actual_ciphertext, actual_ciphertext_valid,
75 +actual_tag, actual_tag_valid, actual_tag_size, _, _, _, _}:
76 tag_size => tag_valid => ciphertext_valid =>
77 +actual_valid = AES.core_bytes_valid_proof(actual_ciphertext,
78 actual_ciphertext_valid)
79 +actual_tag_value = {AES.Tag{actual_tag, actual_tag_size,
80 AES.core_bytes_valid_proof(actual_tag, actual_tag_valid)} :
81 AES.Tag}
82 +expected_tag_value = {AES.Tag{tag_bytes, tag_size, tag_valid} :
83 AES.Tag}
84 tag_eq = tag_equal(actual_tag, actual_tag_size,
85 AES.core_bytes_valid_proof(actual_tag, actual_tag_valid),
86 tag_bytes, tag_matches, tag_size, tag_valid)
87 envelope_eq = envelope_equal(nonce, actual_ciphertext,
88 actual_tag_value, actual_valid, ciphertext,
89 expected_tag_value, ciphertext_matches, tag_eq,
90 ciphertext_valid)
91 Equal.cong(AES.Envelope,
92 Result<&2, &2, AES.Error, AES.Envelope>, value => Done{value},
93 AES.envelope_from_gcm_checked(nonce, output),
94 AES.Envelope{nonce, ciphertext, expected_tag_value,
95 ciphertext_valid}, envelope_eq)
96
97def encrypt_matches(+key: AES.SecretKey, +nonce: AES.Nonce,
98 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
99 +ciphertext: List<&2, U32>, +tag_bytes: List<&2, U32>,
100 aad_valid: {AES.aad_valid(aad) == True{} : Bool},
101 plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
102 ciphertext_matches: {Fields.output_ciphertext(AES.encrypt_valid_output(
103 key, nonce, aad, plaintext)) == ciphertext : List<&2, U32>},
104 tag_matches: {Fields.output_tag(AES.encrypt_valid_output(key, nonce, aad,
105 plaintext)) == tag_bytes : List<&2, U32>},
106 +tag_size: {List.length(&2, U32, tag_bytes) == 16n : Nat},
107 +tag_valid: {AES.bytes_valid(tag_bytes) == True{} : Bool},
108 +ciphertext_valid: {AES.bytes_valid(ciphertext) == True{} : Bool}) ->
109 {AES.encrypt(key, nonce, aad, plaintext) ==
110 Done{AES.Envelope{nonce, ciphertext,
111 AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}} :
112 Result<&2, &2, AES.Error, AES.Envelope>}:
113 aad_checked = Equal.cong(Bool,
114 Result<&2, &2, AES.Error, AES.Envelope>,
115 flag => AES.encrypt_checked(key, nonce, aad, plaintext, flag,
116 AES.plaintext_valid(plaintext)), AES.aad_valid(aad), True{},
117 aad_valid)
118 plaintext_checked = Equal.cong(Bool,
119 Result<&2, &2, AES.Error, AES.Envelope>,
120 flag => AES.encrypt_checked(key, nonce, aad, plaintext, True{}, flag),
121 AES.plaintext_valid(plaintext), True{}, plaintext_valid)
122 output_eq = output_matches(nonce,
123 AES.encrypt_valid_output(key, nonce, aad, plaintext), ciphertext,
124 tag_bytes, ciphertext_matches, tag_matches, tag_size, tag_valid,
125 ciphertext_valid)
126 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
127 AES.encrypt(key, nonce, aad, plaintext),
128 AES.encrypt_valid(key, nonce, aad, plaintext),
129 Done{AES.Envelope{nonce, ciphertext,
130 AES.Tag{tag_bytes, tag_size, tag_valid}, ciphertext_valid}},
131 Equal.trans(Result<&2, &2, AES.Error, AES.Envelope>,
132 AES.encrypt(key, nonce, aad, plaintext),
133 AES.encrypt_checked(key, nonce, aad, plaintext, True{},
134 AES.plaintext_valid(plaintext)),
135 AES.encrypt_valid(key, nonce, aad, plaintext),
136 aad_checked, plaintext_checked), output_eq)