LAWS.bend

bend-osdev-aead@0.1.0.0 · 166 lines · 9 definitions

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.
21import Base
22import bend-osdev-bytes@0.1.0.0/bytes.bend as B
23import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
24import bend-osdev-aead@0.1.0.0/aead.bend as Ad
25import bend-osdev-aead@0.1.0.0/aesround.bend as R
26import bend-osdev-aead@0.1.0.0/aegis128.bend as G
27import bend-osdev-aead@0.1.0.0/authenc.bend as Au
28import bend-osdev-aead@0.1.0.0/essiv.bend as Es
29import bend-osdev-aead@0.1.0.0/seqiv.bend as Sq
30import bend-osdev-aead@0.1.0.0/echainiv.bend as Ec
31
32# AEGIS-128 (aegis128.bend)
33
34law 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
43law 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
56law 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
61law 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
79law 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<KE, KM>
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
97law 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
113law 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
134law 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
148law 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>}