proof/AES_TagRejectProof.bend

qasim-bend-kit@0.1.0.2 · 40 lines · 2 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_TagCompareProof.bend as Compare
5
6def rejects_comparison(+words: List<&2, U32>,
7    +envelope: AES.Envelope, +supplied: List<&2, U32>,
8    +expected: List<&2, U32>,
9    changed: {supplied != expected : List<&2, U32>}) ->
10    {AES.decrypt_auth_result(words, envelope,
11        AES.bytes_equal_full_scan(supplied, expected)) ==
12     Fail{AES.AuthenticationFailed{}} :
13        Result<&2, &2, AES.Error, List<&2, U32>>}:
14    Equal.cong(Bool, Result<&2, &2, AES.Error, List<&2, U32>>,
15        authenticated => AES.decrypt_auth_result(words, envelope,
16            authenticated),
17        AES.bytes_equal_full_scan(supplied, expected), False{},
18        Compare.unequal_is_false(supplied, expected, changed))
19
20def rejects_tag(+words: List<&2, U32>, +nonce: List<&2, U32>,
21    +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
22    +envelope: AES.Envelope, +tag: AES.Tag,
23    +original: List<&2, U32>,
24    canonical: {original == Core.gcm_tag_bytes(Core.gcm_tag_output(
25        words, nonce, aad, ciphertext)) : List<&2, U32>},
26    changed: {AES.tag_bytes(tag) != original : List<&2, U32>}) ->
27    {AES.decrypt_authenticated_tag(words, nonce, aad, ciphertext, envelope,
28        tag) == Fail{AES.AuthenticationFailed{}} :
29        Result<&2, &2, AES.Error, List<&2, U32>>}:
30    match tag:
31        case AES.Tag{bytes, size, valid}:
32            rejects_comparison(words, envelope, bytes,
33                Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
34                    ciphertext)),
35                same => changed(Equal.trans(List<&2, U32>, bytes,
36                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
37                        aad, ciphertext)), original, same,
38                    Equal.sym(List<&2, U32>, original,
39                        Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce,
40                            aad, ciphertext)), canonical))))