check.bend

bend-osdev-aria@0.1.0.0 · 93 lines · 0 definitions

1# ARIA: RFC 5794's three vectors, both ways (the ciphertext, then the
2# plaintext decrypted back), and ARIA-128 through cbc's CBC over
3# 32 KB both ways.
4import Base
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
7import bend-osdev-cbc@0.1.0.0/cbc.bend as CB
8import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
9import bend-osdev-aria@0.1.0.0/aria.bend as A
10
11def b128.of(m: Maybe<&2, M.CmBlock>) -> M.CmBlock:
12  match m:
13    case None{}:
14      M.CmBlock.zero()
15    case Some{b}:
16      b
17
18def b128(o: B.Octets) -> M.CmBlock:
19  b128.of(M.CmBlock.of_octets(o))
20
21def key(~K: Data, r: Result<&2, &2, L.LcError, K>, d: K) -> K:
22  match r:
23    case Fail{e}:
24      d
25    case Done{k}:
26      k
27
28def both(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, b: M.CmBlock) -> String:
29  +c = enc(k, b)
30  M.CmBlock.hex(c) ++ " " ++ M.CmBlock.hex(dec(k, c))
31
32def aria_key(k: B.Octets) -> A.LcAriaKey:
33  key(~A.LcAriaKey, A.LcAria.key(k), A.LcAriaKey{Nil{}})
34
35def aria(k: B.Octets, b: B.Octets) -> String:
36  both(~A.LcAriaKey, ~A.LcAria.encrypt, ~A.LcAria.decrypt, aria_key(k), b128(b))
37
38# n bytes, byte i = 7i + 3 (mod 256)
39def big.go(n: Nat, +i: U32, acc: List<&2, U32>) -> List<&2, U32>:
40  match n:
41    case 0n:
42      B.rev(acc)
43    case 1n+p:
44      big.go(p, U32.add(i, 1), Con{U32.and(255, U32.add(U32.mul(i, 7), 3)), acc})
45
46def big(n: Nat) -> B.Octets:
47  B.Octets.of_list(big.go(n, 0, Nil{}))
48
49def iv16() -> B.Octets:
50  B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15])
51
52def last16(r: Result<&2, &2, M.CmError, B.Octets>) -> String:
53  match r:
54    case Fail{e}:
55      "fail"
56    case Done{+o}:
57      B.Octets.hex(B.Octets.drop(Nat.sub(B.Octets.len(o), 16n), o))
58
59def verdict(b: Bool) -> String:
60  match b:
61    case True{}:
62      "ok"
63    case False{}:
64      "differs"
65
66def same(r: Result<&2, &2, M.CmError, B.Octets>, +m: B.Octets) -> String:
67  match r:
68    case Fail{e}:
69      "fail"
70    case Done{o}:
71      verdict(B.Octets.is_eq(o, m))
72
73def cbc128(~K: Data, ~enc: K -> M.CmBlock -> M.CmBlock, ~dec: K -> M.CmBlock -> M.CmBlock, +k: K, n: Nat) -> String:
74  +m = big(n)
75  +c = CB.Cbc.encrypt(~K, ~enc, k, iv16(), m)
76  last16(c) ++ " " ++ same(Result.bind(&2, &2, M.CmError, B.Octets, B.Octets, c, x => CB.Cbc.decrypt(~K, ~dec, k, iv16(), x)), m)
77
78def aria_cbc(k: B.Octets, n: Nat) -> String:
79  cbc128(~A.LcAriaKey, ~A.LcAria.encrypt, ~A.LcAria.decrypt, aria_key(k), n)
80
81# BEGIN GENERATED by gen/vectors.py: check
82def main() -> IO(Unit):
83  do IO<Unit>:
84    IO.print(aria(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]), B.Octets.of_list([0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255])))
85    IO.print(aria(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23]), B.Octets.of_list([0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255])))
86    IO.print(aria(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31]), B.Octets.of_list([0, 17, 34, 51, 68, 85, 102, 119, 136, 153, 170, 187, 204, 221, 238, 255])))
87    IO.print(aria_cbc(B.Octets.of_list([1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16]), 32768n))
88
89#|d718fbd6ab644c739da95f3be6451778 00112233445566778899aabbccddeeff
90#|26449c1805dbe7aa25a468ce263a9e79 00112233445566778899aabbccddeeff
91#|f92bd7c79fb72e2f2b8f80c1972d24fc 00112233445566778899aabbccddeeff
92#|78d7ea7c6c947995b6180eeac7c72206 ok
93# END GENERATED: check