1	import Base
2	import ../libs/AES256GCM.bend as AES
3	import ../libs/AES256GCMCore.bend as Core
4	import ./AES_EncryptProof.bend as Encrypt
5	import ./AES_TagRejectProof.bend as Reject
6	
7	def 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	
38	def 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	
69	def 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)