def canonical_for_equal_envelope

qasim-bend-kit@0.1.0.2 · proof/AES_TamperProof.bend:7

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

7def 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))