1 # Laws about the public interface of the aead package. 2 # 3 # Every construction is an AEAD of the crypto package's AEAD interface, 4 # whose round-trip law is stated as there: open accepts what seal produced 5 # and gives the plaintext back, and when seal refuses, open-after-seal 6 # refuses alike, 7 # bind(seal(k, n, a, p), c => open(k, n, a, c)) == map(c => p, seal(k, n, a, p)) 8 # 9 # AEGIS-128 satisfies it for every key, nonce, associated data and message. 10 # The generic constructions satisfy it wherever what they are built from 11 # does, at the very arguments they use (a hypothesis h, used once: crypto's 12 # README, "How the laws are stated"): encrypt-then-MAC wherever its cipher's 13 # decryption undoes its encryption, ESSIV wherever the wrapped cipher or 14 # AEAD undoes itself at the derived IV, seqiv and echainiv wherever the 15 # wrapped AEAD does at the generated IV (of the nonce's length, hl). 16 # 17 # A changed tag: AEGIS-128 and encrypt-then-MAC refuse every tag but the one 18 # they compute (CrTagMismatch), for every key, nonce, associated data and 19 # ciphertext; a forgery's chance of hitting the right tag is 2^-8tlen, a 20 # matter of the MAC's or AEGIS's security, not of a law. 21 import Base 22 import bend-osdev-bytes@0.1.0.0/bytes.bend as B 23 import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr 24 import ./aead.bend as Ad 25 import ./aesround.bend as R 26 import ./aegis128.bend as G 27 import ./authenc.bend as Au 28 import ./essiv.bend as Es 29 import ./seqiv.bend as Sq 30 import ./echainiv.bend as Ec 31 32 # AEGIS-128 (aegis128.bend) 33 34 law aegis128_round_trip: 35 for +k: G.AdAegisKey 36 for +n: B.Octets 37 for +a: B.Octets 38 for +p: B.Octets 39 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, G.AdAegis128.seal(k, n, a, p), c => G.AdAegis128.open(k, n, a, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, G.AdAegis128.seal(k, n, a, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 40 41 # a tag of 16 bytes other than the one AEGIS-128 computes for the ciphertext 42 # is refused, under a 16-byte nonce 43 law aegis128_tamper: 44 for +k: G.AdAegisKey 45 for +n: B.Octets 46 for +a: B.Octets 47 for +c: B.Octets 48 for +t: B.Octets 49 for hn: {B.Octets.len(n) == 16n : Nat} 50 for hl: {B.Octets.len(t) == 16n : Nat} 51 for ht: {Ad.AdTag.is_eq(G.AdAegis128.tag_of(k, n, a, c), t) == False{} : Bool} 52 {G.AdAegis128.open(k, n, a, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>} 53 54 # RFC 10032, Appendix A.1: AESRound(000102..0f, 101112..1f) = 55 # 7a7b4e5638782546a8c0477a3b813f43 56 law aesround_rfc10032: 57 {R.AdAes.round(R.AdAes.sbox(), R.AdBlk{66051, 67438087, 134810123, 202182159}, R.AdBlk{269554195, 336926231, 404298267, 471670303}) == R.AdBlk{2054901334, 947397958, 2831173498, 998326083} : R.AdBlk} 58 59 # Encrypt-then-MAC (authenc.bend), over every cipher and MAC 60 61 law authenc_round_trip_if: 62 for ~KE: Data 63 for ~KM: Data 64 for ~enc: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 65 for ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 66 for ~mac: KM -> B.Octets -> B.Octets 67 for ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets 68 for ~tlen: Nat 69 for +ke: KE 70 for +km: KM 71 for +iv: B.Octets 72 for +aad: B.Octets 73 for +p: B.Octets 74 for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, enc(ke, iv, p), c => dec(ke, iv, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, enc(ke, iv, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 75 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Au.AdAuthenc.seal(~KE, ~KM, ~enc, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, p), c => Au.AdAuthenc.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Au.AdAuthenc.seal(~KE, ~KM, ~enc, ~mac, ~input, ~tlen, Au.AdAuthencKey{ke, km}, iv, aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 76 77 # a tag of tlen bytes other than the computed one is refused, and the 78 # cipher never runs 79 law authenc_tamper: 80 for ~KE: Data 81 for ~KM: Data 82 for ~dec: KE -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 83 for ~mac: KM -> B.Octets -> B.Octets 84 for ~input: B.Octets -> B.Octets -> B.Octets -> B.Octets 85 for ~tlen: Nat 86 for +k: Au.AdAuthencKey 87 for +iv: B.Octets 88 for +aad: B.Octets 89 for +c: B.Octets 90 for +t: B.Octets 91 for hl: {B.Octets.len(t) == tlen : Nat} 92 for ht: {Ad.AdTag.is_eq(Au.AdAuthenc.tag(~KE, ~KM, ~mac, ~input, ~tlen, k, aad, iv, c), t) == False{} : Bool} 93 {Au.AdAuthenc.open(~KE, ~KM, ~dec, ~mac, ~input, ~tlen, k, iv, aad, B.Octets.append(c, t)) == Fail{Cr.CrTagMismatch{}} : Result<&2, &2, Cr.CrError, B.Octets>} 94 95 # ESSIV (essiv.bend): over a cipher with an IV, and over an AEAD 96 97 law essiv_round_trip_if: 98 for ~KD: Data 99 for ~KS: Data 100 for ~Blk: Data 101 for ~enc: KS -> Blk -> Blk 102 for ~blk_of: B.Octets -> Maybe<&2, Blk> 103 for ~blk_to: Blk -> B.Octets 104 for ~cenc: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 105 for ~cdec: KD -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 106 for +kd: KD 107 for +ks: KS 108 for +iv: B.Octets 109 for +m: B.Octets 110 for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, cenc(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), m), c => cdec(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => m, cenc(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), m)) : Result<&2, &2, Cr.CrError, B.Octets>} 111 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Es.AdEssiv.encrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cenc, Es.AdEssivKey{kd, ks}, iv, m), c => Es.AdEssiv.decrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cdec, Es.AdEssivKey{kd, ks}, iv, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => m, Es.AdEssiv.encrypt(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~cenc, Es.AdEssivKey{kd, ks}, iv, m)) : Result<&2, &2, Cr.CrError, B.Octets>} 112 113 law essiv_aead_round_trip_if: 114 for ~KD: Data 115 for ~KS: Data 116 for ~Blk: Data 117 for ~enc: KS -> Blk -> Blk 118 for ~blk_of: B.Octets -> Maybe<&2, Blk> 119 for ~blk_to: Blk -> B.Octets 120 for ~seal: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 121 for ~open: KD -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 122 for +kd: KD 123 for +ks: KS 124 for +iv: B.Octets 125 for +aad: B.Octets 126 for +p: B.Octets 127 for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, seal(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), aad, p), c => open(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, seal(kd, Es.AdEssiv.iv(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, Es.AdEssivKey{kd, ks}, iv), aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 128 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Es.AdEssiv.seal(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, Es.AdEssivKey{kd, ks}, iv, aad, p), c => Es.AdEssiv.open(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~open, Es.AdEssivKey{kd, ks}, iv, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Es.AdEssiv.seal(~KD, ~KS, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, Es.AdEssivKey{kd, ks}, iv, aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 129 130 # seqiv (seqiv.bend) and echainiv (echainiv.bend): the generated IV, ivlen 131 # bytes long (hl), travels in front of the ciphertext, and the wrapped AEAD 132 # authenticates it as associated data after A 133 134 law seqiv_round_trip_if: 135 for ~KA: Data 136 for ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 137 for ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 138 for ~ivlen: Nat 139 for +ka: KA 140 for +salt: B.Octets 141 for +seq: B.Octets 142 for +aad: B.Octets 143 for +p: B.Octets 144 for hl: {B.Octets.len(Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)) == ivlen : Nat} 145 for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, seal(ka, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq), B.Octets.append(aad, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)), p), c => open(ka, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq), B.Octets.append(aad, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, seal(ka, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq), B.Octets.append(aad, Sq.AdSeqiv.iv(~KA, Sq.AdSeqivKey{ka, salt}, seq)), p)) : Result<&2, &2, Cr.CrError, B.Octets>} 146 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Sq.AdSeqiv.seal(~KA, ~seal, Sq.AdSeqivKey{ka, salt}, seq, aad, p), c => Sq.AdSeqiv.open(~KA, ~open, ~ivlen, Sq.AdSeqivKey{ka, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Sq.AdSeqiv.seal(~KA, ~seal, Sq.AdSeqivKey{ka, salt}, seq, aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>} 147 148 law echainiv_round_trip_if: 149 for ~KA: Data 150 for ~KC: Data 151 for ~Blk: Data 152 for ~enc: KC -> Blk -> Blk 153 for ~blk_of: B.Octets -> Maybe<&2, Blk> 154 for ~blk_to: Blk -> B.Octets 155 for ~seal: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 156 for ~open: KA -> B.Octets -> B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, B.Octets> 157 for ~ivlen: Nat 158 for +ka: KA 159 for +kc: KC 160 for +salt: B.Octets 161 for +seq: B.Octets 162 for +aad: B.Octets 163 for +p: B.Octets 164 for hl: {B.Octets.len(Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq)) == ivlen : Nat} 165 for h: {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, seal(ka, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq), B.Octets.append(aad, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq)), p), c => open(ka, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq), B.Octets.append(aad, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq)), c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, seal(ka, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq), B.Octets.append(aad, Ec.AdEchainiv.iv(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, Ec.AdEchainivKey{ka, kc, salt}, seq)), p)) : Result<&2, &2, Cr.CrError, B.Octets>} 166 {Result.bind(&2, &2, Cr.CrError, B.Octets, B.Octets, Ec.AdEchainiv.seal(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, Ec.AdEchainivKey{ka, kc, salt}, seq, aad, p), c => Ec.AdEchainiv.open(~KA, ~KC, ~open, ~ivlen, Ec.AdEchainivKey{ka, kc, salt}, seq, aad, c)) == Result.map(&2, &2, Cr.CrError, B.Octets, B.Octets, c => p, Ec.AdEchainiv.seal(~KA, ~KC, ~Blk, ~enc, ~blk_of, ~blk_to, ~seal, Ec.AdEchainivKey{ka, kc, salt}, seq, aad, p)) : Result<&2, &2, Cr.CrError, B.Octets>}