proof/AES_TamperProof.bend
qasim-bend-kit@0.1.0.2 · 119 lines · 3 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_EncryptProof.bend as Encrypt
5import qasim-bend-kit@0.1.0.2/proof/AES_TagRejectProof.bend as Reject
6
7def canonical_for_equal_envelope(+words: List<&2, U32>,
8 +nonce: List<&2, U32>, +tampered_nonce: List<&2, U32>,
9 +aad: List<&2, U32>, +ciphertext: List<&2, U32>,
10 +tampered_ciphertext: List<&2, U32>, +original: List<&2, U32>,
11 canonical: {original == Core.gcm_tag_bytes(Core.gcm_tag_output(words,
12 nonce, aad, ciphertext)) : List<&2, U32>},
13 same_nonce: {tampered_nonce == nonce : List<&2, U32>},
14 same_ciphertext: {tampered_ciphertext == ciphertext : List<&2, U32>}) ->
15 {original == Core.gcm_tag_bytes(Core.gcm_tag_output(words,
16 tampered_nonce, aad, tampered_ciphertext)) : List<&2, U32>}:
17 nonce_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>,
18 value => Core.gcm_tag_bytes(Core.gcm_tag_output(words, value, aad,
19 ciphertext)), nonce, tampered_nonce,
20 Equal.sym(List<&2, U32>, tampered_nonce, nonce, same_nonce))
21 ciphertext_rewrite = Equal.cong(List<&2, U32>, List<&2, U32>,
22 value => Core.gcm_tag_bytes(Core.gcm_tag_output(words,
23 tampered_nonce, aad, value)), ciphertext, tampered_ciphertext,
24 Equal.sym(List<&2, U32>, tampered_ciphertext, ciphertext,
25 same_ciphertext))
26 Equal.trans(List<&2, U32>, original,
27 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad, ciphertext)),
28 Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce, aad,
29 tampered_ciphertext)), canonical,
30 Equal.trans(List<&2, U32>,
31 Core.gcm_tag_bytes(Core.gcm_tag_output(words, nonce, aad,
32 ciphertext)),
33 Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce,
34 aad, ciphertext)),
35 Core.gcm_tag_bytes(Core.gcm_tag_output(words, tampered_nonce,
36 aad, tampered_ciphertext)), nonce_rewrite, ciphertext_rewrite))
37
38def reject_authenticated(+key: AES.SecretKey, +aad: List<&2, U32>,
39 +envelope: AES.Envelope, +tampered: AES.Envelope,
40 canonical: {AES.tag_bytes(AES.envelope_tag(envelope)) ==
41 Core.gcm_tag_bytes(Core.gcm_tag_output(
42 Core.aes256_expand(AES.secret_key_bytes(key)),
43 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)), aad,
44 AES.ciphertext(envelope))) : List<&2, U32>},
45 same_nonce: {AES.raw_nonce_bytes(AES.envelope_nonce(tampered)) ==
46 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) : List<&2, U32>},
47 same_ciphertext: {AES.ciphertext(tampered) == AES.ciphertext(envelope) :
48 List<&2, U32>},
49 changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
50 AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}) ->
51 {AES.decrypt_authenticated(key, aad, tampered) ==
52 Fail{AES.AuthenticationFailed{}} :
53 Result<&2, &2, AES.Error, List<&2, U32>>}:
54 match key envelope tampered:
55 case AES.SecretKey{+key_bytes, _, _}
56 AES.Envelope{nonce, ciphertext, tag, _}
57 AES.Envelope{tampered_nonce, tampered_ciphertext, tampered_tag, _}:
58 +words = Core.aes256_expand(key_bytes)
59 +tampered_nonce_bytes = AES.raw_nonce_bytes(tampered_nonce)
60 +original = AES.tag_bytes(tag)
61 canonical_tampered = canonical_for_equal_envelope(words,
62 AES.raw_nonce_bytes(nonce), tampered_nonce_bytes, aad,
63 ciphertext, tampered_ciphertext, original, canonical,
64 same_nonce, same_ciphertext)
65 Reject.rejects_tag(words, tampered_nonce_bytes, aad,
66 tampered_ciphertext, tampered, tampered_tag, original,
67 canonical_tampered, changed_tag)
68
69def rejects_changed_tag(+key: AES.SecretKey, +nonce: AES.Nonce,
70 +aad: List<&2, U32>, +plaintext: List<&2, U32>,
71 +envelope: AES.Envelope, +tampered: AES.Envelope,
72 +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
73 Result<&2, &2, AES.Error, AES.Envelope>},
74 same_nonce: {AES.raw_nonce_bytes(AES.envelope_nonce(tampered)) ==
75 AES.raw_nonce_bytes(AES.envelope_nonce(envelope)) : List<&2, U32>},
76 +same_ciphertext: {AES.ciphertext(tampered) == AES.ciphertext(envelope) :
77 List<&2, U32>},
78 changed_tag: {AES.tag_bytes(AES.envelope_tag(tampered)) !=
79 AES.tag_bytes(AES.envelope_tag(envelope)) : List<&2, U32>}) ->
80 {AES.decrypt(key, aad, tampered) == Fail{AES.AuthenticationFailed{}} :
81 Result<&2, &2, AES.Error, List<&2, U32>>}:
82 +aad_ok = Encrypt.successful_encrypt_aad_valid(key, nonce, aad,
83 plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
84 {==}, {==}, envelope, encrypted)
85 +plaintext_ok = Encrypt.successful_encrypt_plaintext_valid(key, nonce,
86 aad, plaintext, AES.aad_valid(aad), AES.plaintext_valid(plaintext),
87 {==}, {==}, envelope, encrypted)
88 ciphertext_ok = Encrypt.successful_encrypt_ciphertext_valid(key, nonce,
89 aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
90 tampered_ciphertext_ok = Equal.trans(Bool,
91 AES.plaintext_valid(AES.ciphertext(tampered)),
92 AES.plaintext_valid(AES.ciphertext(envelope)), True{},
93 Equal.cong(List<&2, U32>, Bool, value => AES.plaintext_valid(value),
94 AES.ciphertext(tampered), AES.ciphertext(envelope),
95 same_ciphertext), ciphertext_ok)
96 canonical = Encrypt.successful_encrypt_envelope_tag_canonical(key,
97 nonce, aad, plaintext, envelope, aad_ok, plaintext_ok, encrypted)
98 rejected = reject_authenticated(key, aad, envelope, tampered,
99 canonical, same_nonce, same_ciphertext, changed_tag)
100 aad_checked = Equal.cong(Bool,
101 Result<&2, &2, AES.Error, List<&2, U32>>,
102 flag => AES.decrypt_checked(key, aad, tampered, flag,
103 AES.plaintext_valid(AES.ciphertext(tampered))),
104 AES.aad_valid(aad), True{}, aad_ok)
105 ciphertext_checked = Equal.cong(Bool,
106 Result<&2, &2, AES.Error, List<&2, U32>>,
107 flag => AES.decrypt_checked(key, aad, tampered, True{}, flag),
108 AES.plaintext_valid(AES.ciphertext(tampered)), True{},
109 tampered_ciphertext_ok)
110 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
111 AES.decrypt(key, aad, tampered),
112 AES.decrypt_checked(key, aad, tampered, True{}, True{}),
113 Fail{AES.AuthenticationFailed{}},
114 Equal.trans(Result<&2, &2, AES.Error, List<&2, U32>>,
115 AES.decrypt(key, aad, tampered),
116 AES.decrypt_checked(key, aad, tampered, True{},
117 AES.plaintext_valid(AES.ciphertext(tampered))),
118 AES.decrypt_checked(key, aad, tampered, True{}, True{}),
119 aad_checked, ciphertext_checked), rejected)