law aes256gcm_preserves_nonce

qasim-bend-kit@0.1.0.2 · LAWS.bend:371

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

371law aes256gcm_preserves_nonce:
372    for +key: AES.SecretKey
373    for +nonce: AES.Nonce
374    for +aad: List<&2, U32>
375    for +plaintext: List<&2, U32>
376    for +envelope: AES.Envelope
377    for encrypted: {AES.encrypt(key, nonce, aad, plaintext) == Done{envelope} :
378        Result<&2, &2, AES.Error, AES.Envelope>}
379    {AES.envelope_nonce(envelope) == nonce : AES.Nonce}

Uses (10)

Used by (0)

No other definition uses this definition.