inst_cm.bend

bend-osdev-crypto@0.1.0.0 · 88 lines · 10 definitions

1# The adapter for cipher-modes: its error type mapped onto CrError, and the
2# block format of its 128-bit block CmBlock (an open type: four big-endian
3# 32-bit words), for every 128-bit cipher that uses it (cipher-modes' AES,
4# legacy-ciphers' SM4, Camellia, Serpent and Twofish).
5#
6# The format's conversions are written here, on the open type, so that its
7# law (format: blk_of(blk_to(b)) == Some{b}) is proved in this package:
8# cipher-modes proves the same of its own CmBlock.of_octets and
9# CmBlock.to_octets, but its PROOF.bend cannot be imported by a proof that
10# passes --verdict (README.md, "Laws").
11import Base
12import bend-osdev-bytes@0.1.0.0/bytes.bend as B
13import bend-osdev-word64@0.1.0.0/word64.bend as W
14import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
15import bend-osdev-crypto@0.1.0.0/crypto.bend as Cr
16
17# Errors
18
19def CrCm.err(e: M.CmError) -> Cr.CrError:
20  match e:
21    case M.CmBadKeyLength{n}:
22      Cr.CrBadKeyLength{n}
23    case M.CmBadIvLength{n}:
24      Cr.CrBadIvLength{n}
25    case M.CmBadTweakLength{n}:
26      Cr.CrBadIvLength{n}
27    case M.CmBadNonceLength{n}:
28      Cr.CrBadNonceLength{n}
29    case M.CmBadTagLength{n}:
30      Cr.CrBadTagLength{n}
31    case M.CmBadBlockSize{n}:
32      Cr.CrBadBlockSize{n}
33    case M.CmNotBlockMultiple{n}:
34      Cr.CrNotBlockMultiple{n}
35    case M.CmTooShort{n}:
36      Cr.CrTooShort{n}
37    case M.CmTooLong{n}:
38      Cr.CrTooLong{n}
39    case M.CmBadPadding{}:
40      Cr.CrBadPadding{}
41    case M.CmTagMismatch{}:
42      Cr.CrTagMismatch{}
43
44# a cipher-modes result as an interface result
45def CrCm.lift(~A: Data, r: Result<&2, &2, M.CmError, A>) -> Result<&2, &2, Cr.CrError, A>:
46  Cr.CrError.lift(~M.CmError, ~A, ~CrCm.err, r)
47
48# a cipher-modes key schedule as the interface's ~key
49def CrCm.key(~K: Data, ~key: B.Octets -> Result<&2, &2, M.CmError, K>, o: B.Octets) -> Result<&2, &2, Cr.CrError, K>:
50  CrCm.lift(~K, key(o))
51
52# The 128-bit block format
53
54def cr.f128.bits8(b: U32) -> Word(8n):
55  match b:
56    case U32{w}:
57      W.W64.bits.lo(8n, 24n, w)
58
59# the word with bytes a, b, c, d, most significant first
60def cr.f128.word(a: U32, b: U32, c: U32, d: U32) -> U32:
61  U32{W.W64.bits.cat(8n, 24n, cr.f128.bits8(d), W.W64.bits.cat(8n, 16n, cr.f128.bits8(c), W.W64.bits.cat(8n, 8n, cr.f128.bits8(b), cr.f128.bits8(a))))}
62
63# the 16 bytes of a block, most significant byte of w0 first
64def cr.f128.bytes(b: M.CmBlock) -> List<&2, U32>:
65  match b:
66    case M.CmBlock{w0, w1, w2, w3}:
67      B.append(B.be32(w0), B.append(B.be32(w1), B.append(B.be32(w2), B.be32(w3))))
68
69# exactly 16 bytes as a block
70def cr.f128.block(xs: List<&2, U32>) -> Maybe<&2, M.CmBlock>:
71  match xs:
72    case Con{a0, Con{a1, Con{a2, Con{a3, Con{a4, Con{a5, Con{a6, Con{a7, Con{a8, Con{a9, Con{a10, Con{a11, Con{a12, Con{a13, Con{a14, Con{a15, Nil{}}}}}}}}}}}}}}}}}:
73      Some{M.CmBlock{cr.f128.word(a0, a1, a2, a3), cr.f128.word(a4, a5, a6, a7), cr.f128.word(a8, a9, a10, a11), cr.f128.word(a12, a13, a14, a15)}}
74    case _:
75      None{}
76
77# a block's 16 bytes
78def CrBlk128.to_octets(b: M.CmBlock) -> B.Octets:
79  B.Octets.of_list(cr.f128.bytes(b))
80
81# 16 bytes as a block; None for any other length
82def CrBlk128.of_octets(o: B.Octets) -> Maybe<&2, M.CmBlock>:
83  cr.f128.block(B.Octets.to_list(o))
84
85def CrBlk128.xor(a: M.CmBlock, b: M.CmBlock) -> M.CmBlock:
86  match a b:
87    case M.CmBlock{a0, a1, a2, a3} M.CmBlock{b0, b1, b2, b3}:
88      M.CmBlock{U32.xor(a0, b0), U32.xor(a1, b1), U32.xor(a2, b2), U32.xor(a3, b3)}