def checked_encrypt

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

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

78def checked_encrypt(+key: AES.SecretKey, +nonce: AES.Nonce,
79    +aad: List<&2, U32>, +plaintext: List<&2, U32>,
80    aad_ok: {AES.aad_valid(aad) == True{} : Bool},
81    plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}) ->
82    {L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)) ==
83     expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext) : List<&2, U32>}:
84    Equal.trans(List<&2, U32>,
85        L.aes256gcm_nist_encrypt_observation(AES.encrypt(key, nonce, aad, plaintext)),
86        L.aes256gcm_nist_encrypt_observation(AES.encrypt_valid(key, nonce, aad, plaintext)),
87        expanded(Core.aes256_expand(AES.secret_key_bytes(key)), nonce, aad, plaintext),
88        Equal.trans(List<&2, U32>,
89            L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
90                AES.aad_valid(aad), AES.plaintext_valid(plaintext))),
91            L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
92                True{}, AES.plaintext_valid(plaintext))),
93            L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
94                True{}, True{})),
95            Equal.cong(Bool, List<&2, U32>, flag =>
96                L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
97                    flag, AES.plaintext_valid(plaintext))),
98                AES.aad_valid(aad), True{}, aad_ok),
99            Equal.cong(Bool, List<&2, U32>, flag =>
100                L.aes256gcm_nist_encrypt_observation(AES.encrypt_checked(key, nonce, aad, plaintext,
101                    True{}, flag)),
102                AES.plaintext_valid(plaintext), True{}, plaintext_ok)),
103        valid_encrypt(key, nonce, aad, plaintext))