stream.bend

bend-osdev-crypto@0.1.0.0 · 115 lines · 15 definitions

1# The stream-cipher interface, and stream ciphers built from a keystream
2# generator.
3#
4# The interface (template arguments, in this order):
5#   ~S: Data                                    the state: key, IV and position
6#   ~O: Data                                    what one step answers
7#   ~start: B.Octets -> B.Octets -> Result<&2, &2, CrError, S>
8#                                               the state for a key and an IV
9#                                               (a cipher without an IV takes
10#                                               the empty one)
11#   ~update: S -> B.Octets -> O                 the next piece of data,
12#                                               encrypted or decrypted (the
13#                                               same thing)
14#   ~out_state: O -> S                          the state after the piece
15#   ~out_data: O -> B.Octets                    the piece encrypted
16# Laws, for every state and all data (README.md, "Laws"):
17#   involution       out_data(update(s, out_data(update(s, m)))) == m
18#   streaming_data   out_data(update(s, a ++ b)) == out_data(update(s, a)) ++
19#                    out_data(update(out_state(update(s, a)), b))
20#   streaming_state  out_state(update(s, a ++ b)) ==
21#                    out_state(update(out_state(update(s, a)), b))
22#
23# Keystream generation is the extension point: CrXor turns any function that
24# gives the next keystream byte and the next state (~next: S ->
25# CrKsStep<S>) into a stream cipher with exactly this interface, and LAWS.bend
26# proves its three laws for every such function, once. CTR mode (modes.bend)
27# is one; RC4 (inst_rc4.bend) satisfies the interface directly.
28import Base
29import bend-osdev-bytes@0.1.0.0/bytes.bend as B
30import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
31
32# A stream cipher in one call: the data under a key and an IV
33def CrStream.crypt(~S: Data, ~O: Data, ~start: B.Octets -> B.Octets -> Result<&2, &2, Cr.CrError, S>, ~update: S -> B.Octets -> O, ~out_data: O -> B.Octets, key: B.Octets, iv: B.Octets, m: B.Octets) -> Result<&2, &2, Cr.CrError, B.Octets>:
34  Result.map(&2, &2, Cr.CrError, S, B.Octets, s => out_data(update(s, m)), start(key, iv))
35
36# The next n keystream bytes (the data n zero bytes)
37def CrStream.keystream(~S: Data, ~O: Data, ~update: S -> B.Octets -> O, ~out_data: O -> B.Octets, s: S, n: Nat) -> B.Octets:
38  out_data(update(s, B.Octets.zeros(n)))
39
40# Keystream generators
41
42# one keystream byte and the state after it
43type CrKsStep<-S: Data> is Data:
44  CrKsStep{k: U32, st: S}
45
46# what CrXor.update answers: the state after the data, and the data
47# encrypted (open type)
48type CrXorOut<-S: Data> is Data:
49  CrXorOut{state: S, data: B.Octets}
50
51def CrKsStep.k(~S: Data, r: CrKsStep<S>) -> U32:
52  match r:
53    case CrKsStep{k, st}:
54      k
55
56def CrKsStep.st(~S: Data, r: CrKsStep<S>) -> S:
57  match r:
58    case CrKsStep{k, st}:
59      st
60
61# The structural forms the proofs reason about: the data, byte by byte, and
62# the state after it
63def cr.ks.xs(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S) -> List<&2, U32>:
64  match ys:
65    case Nil{}:
66      Nil{}
67    case Con{x, t}:
68      Con{B.byte(U32.xor(x, CrKsStep.k(~S, next(s)))), cr.ks.xs(~S, ~next, t, CrKsStep.st(~S, next(s)))}
69
70def cr.ks.after(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S) -> S:
71  match ys:
72    case Nil{}:
73      s
74    case Con{x, t}:
75      cr.ks.after(~S, ~next, t, CrKsStep.st(~S, next(s)))
76
77# The loop that runs: tail-recursive, the output kept reversed, each
78# keystream byte computed once
79type CrKsRun<-S: Data> is Data:
80  CrKsRun{st: S, rev: List<&2, U32>}
81
82def cr.rev_onto(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
83  match xs:
84    case Nil{}:
85      acc
86    case Con{h, t}:
87      cr.rev_onto(t, Con{h, acc})
88
89def cr.ks.go(~S: Data, ~next: S -> CrKsStep<S>, ys: List<&2, U32>, +s: S, acc: List<&2, U32>) -> CrKsRun<S>:
90  match ys:
91    case Nil{}:
92      CrKsRun{s, acc}
93    case Con{x, t}:
94      +r = next(s)
95      cr.ks.go(~S, ~next, t, CrKsStep.st(~S, r), Con{B.byte(U32.xor(x, CrKsStep.k(~S, r))), acc})
96
97def cr.ks.out(~S: Data, r: CrKsRun<S>) -> CrXorOut<S>:
98  match r:
99    case CrKsRun{st, rev}:
100      CrXorOut{st, B.Octets.of_list(cr.rev_onto(rev, Nil{}))}
101
102# The stream cipher of a keystream generator: m XORed with the next len(m)
103# keystream bytes, and the state after them
104def CrXor.update(~S: Data, ~next: S -> CrKsStep<S>, s: S, m: B.Octets) -> CrXorOut<S>:
105  cr.ks.out(~S, cr.ks.go(~S, ~next, B.Octets.to_list(m), s, Nil{}))
106
107def CrXor.out_state(~S: Data, o: CrXorOut<S>) -> S:
108  match o:
109    case CrXorOut{st, d}:
110      st
111
112def CrXor.out_data(~S: Data, o: CrXorOut<S>) -> B.Octets:
113  match o:
114    case CrXorOut{st, d}:
115      d