def successful_encrypt_ciphertext_matches_ctr

qasim-bend-kit@0.1.0.2 · proof/AES_EncryptProof.bend:323

import Base
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
import qasim-bend-kit@0.1.0.2/proof/AES_CoreTagProof.bend as CoreTagProof

323def successful_encrypt_ciphertext_matches_ctr(+key: AES.SecretKey,
324    +nonce: AES.Nonce, +aad: List<&2, U32>,
325    +plaintext: List<&2, U32>, +envelope: AES.Envelope,
326    aad_valid: {AES.aad_valid(aad) == True{} : Bool},
327    plaintext_valid: {AES.plaintext_valid(plaintext) == True{} : Bool},
328    +encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
329        Result<&2, &2, AES.Error, AES.Envelope>}) ->
330    {AES.ciphertext(envelope) ==
331     Core.gcm_zip_xor(plaintext,
332        Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
333            Core.aes256_expand(AES.secret_key_bytes(key)),
334            Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))) :
335        List<&2, U32>}:
336    Equal.trans(List<&2, U32>,
337        AES.ciphertext(envelope),
338        CoreTagProof.output_ciphertext(AES.encrypt_valid_output(key, nonce,
339            aad, plaintext)),
340        Core.gcm_zip_xor(plaintext,
341            Core.gcm_ctr_stream_exact(List.length(&2, U32, plaintext),
342                Core.aes256_expand(AES.secret_key_bytes(key)),
343                Core.gcm_inc32(Core.gcm_j0(AES.raw_nonce_bytes(nonce))))),
344        successful_encrypt_ciphertext_matches_gcm(key, nonce, aad,
345            plaintext, envelope, aad_valid, plaintext_valid, encrypted),
346        CoreTagProof.raw_encrypt_output_ciphertext(
347            AES.secret_key_bytes(key), AES.raw_nonce_bytes(nonce), aad,
348            plaintext))