def finish_encrypt

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:105

import Base
import qasim-bend-kit@0.1.0.2/LAWS.bend as L
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

105def finish_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
106    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
107    +words: List<&2, U32>, +bytes: List<&2, U32>, +tag: List<&2, U32>,
108    aad_ok: {AES.aad_valid(aad) == True{} : Bool},
109    plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool},
110    key_matches: {Core.aes256_expand(AES.secret_key_bytes(key)) == words : List<&2, U32>},
111    ciphertext_matches: {ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)) == bytes : List<&2, U32>},
112    tag_matches: {Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)) == tag : List<&2, U32>}) ->
113    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) ==
114     List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)) : List<&2, U32>}:
115    Equal.trans(List<&2, U32>,
116        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
117        expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
118        List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
119        checked_encrypt(key, nonce, aad, plaintext, aad_ok, plaintext_ok),
120        Equal.trans(List<&2, U32>,
121            expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
122            expanded(words, nonce, aad, plaintext),
123            List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
124            Equal.cong(List<&2, U32>, List<&2, U32>, expanded_words =>
125                expanded(expanded_words, nonce, aad, plaintext),
126                Core.aes256_expand(AES.secret_key_bytes(key)), words, key_matches),
127            Equal.trans(List<&2, U32>, expanded(words, nonce, aad, plaintext),
128                parts(words, nonce, aad, bytes),
129                List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag)),
130                Equal.cong(List<&2, U32>, List<&2, U32>, encrypted => parts(words, nonce, aad, encrypted),
131                    ciphertext(Core.gcm_ctr_encrypt(words, AES.raw_nonce_bytes(nonce), plaintext)), bytes,
132                    ciphertext_matches),
133                Equal.cong(List<&2, U32>, List<&2, U32>, tag_bytes =>
134                    List.append(&2, U32, AES.raw_nonce_bytes(nonce), List.append(&2, U32, bytes, tag_bytes)),
135                    Core.gcm_tag_bytes(Core.gcm_tag_output(words, AES.raw_nonce_bytes(nonce), aad, bytes)),
136                    tag, tag_matches))))