PROOF.bend
bend-osdev-camellia@0.1.0.0 · 146 lines · 0 definitions
1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
4import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
5import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
6import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as CoreP
7import bend-osdev-camellia@0.1.0.0/camellia.bend as C
8import bend-osdev-camellia@0.1.0.0/LAWS.bend as Laws
9
10def block_xx(s: M.CmBlock, k: M.CmBlock) -> {s == M.CmBlock.xor(M.CmBlock.xor(s, k), k) : M.CmBlock}:
11 match s k:
12 case M.CmBlock{+a0, +a1, +a2, +a3} M.CmBlock{+b0, +b1, +b2, +b3}:
13 %CoreL.u32_xor_cancel(a0, b0) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{_, U32.xor(U32.xor(a1, b1), b1), U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
14 %CoreL.u32_xor_cancel(a1, b1) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, _, U32.xor(U32.xor(a2, b2), b2), U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
15 %CoreL.u32_xor_cancel(a2, b2) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, _, U32.xor(U32.xor(a3, b3), b3)} : M.CmBlock}
16 %CoreL.u32_xor_cancel(a3, b3) : {M.CmBlock{a0, a1, a2, a3} == M.CmBlock{a0, a1, a2, _} : M.CmBlock}
17 {==}
18
19# Camellia: each step of the cipher is undone (FL by FL^-1 and back, the
20# rounds and whitening by XOR, whatever F is), so the list of steps is
21
22def cam_fl_inv(x: L.LcBlock64, k: L.LcBlock64) -> {x == C.cam.flinv(C.cam.fl(x, k), k) : L.LcBlock64}:
23 match x k:
24 case L.LcBlock64{+x1, +x2} L.LcBlock64{+k1, +k2}:
25 %CoreL.u32_xor_cancel(x1, U32.or(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), k2)) : {L.LcBlock64{x1, x2} == L.LcBlock64{_, U32.xor(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), L.lc.rotl(U32.and(_, k1), 1n))} : L.LcBlock64}
26 %CoreL.u32_xor_cancel(x2, L.lc.rotl(U32.and(x1, k1), 1n)) : {L.LcBlock64{x1, x2} == L.LcBlock64{x1, _} : L.LcBlock64}
27 {==}
28
29def cam_flinv_inv(y: L.LcBlock64, k: L.LcBlock64) -> {y == C.cam.fl(C.cam.flinv(y, k), k) : L.LcBlock64}:
30 match y k:
31 case L.LcBlock64{+y1, +y2} L.LcBlock64{+k1, +k2}:
32 %CoreL.u32_xor_cancel(y2, L.lc.rotl(U32.and(U32.xor(y1, U32.or(y2, k2)), k1), 1n)) : {L.LcBlock64{y1, y2} == L.LcBlock64{U32.xor(U32.xor(y1, U32.or(y2, k2)), U32.or(_, k2)), _} : L.LcBlock64}
33 %CoreL.u32_xor_cancel(y1, U32.or(y2, k2)) : {L.LcBlock64{y1, y2} == L.LcBlock64{_, y2} : L.LcBlock64}
34 {==}
35
36def cam_white(a: L.LcBlock64, b: L.LcBlock64, +s: M.CmBlock) -> {s == C.cam.white(a, b, C.cam.white(a, b, s)) : M.CmBlock}:
37 match a b:
38 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}:
39 block_xx(s, M.CmBlock{a0, a1, b0, b1})
40
41def cam_f1(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF1{t, k}, C.cam.op(C.LcCamF1{t, k}, s)) : M.CmBlock}:
42 match s:
43 case M.CmBlock{+s0, +s1, +s2, +s3}:
44 %CoreL.u32_xor_cancel(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock}
45 %CoreL.u32_xor_cancel(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock}
46 {==}
47
48def cam_f1d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF1{t, k}, C.cam.unop(C.LcCamF1{t, k}, s)) : M.CmBlock}:
49 match s:
50 case M.CmBlock{+s0, +s1, +s2, +s3}:
51 %CoreL.u32_xor_cancel(s2, C.cam.hi(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, _, U32.xor(U32.xor(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k)))} : M.CmBlock}
52 %CoreL.u32_xor_cancel(s3, C.cam.lo(C.cam.f(t, L.LcBlock64{s0, s1}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, s2, _} : M.CmBlock}
53 {==}
54
55def cam_f2(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF2{t, k}, C.cam.op(C.LcCamF2{t, k}, s)) : M.CmBlock}:
56 match s:
57 case M.CmBlock{+s0, +s1, +s2, +s3}:
58 %CoreL.u32_xor_cancel(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock}
59 %CoreL.u32_xor_cancel(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock}
60 {==}
61
62def cam_f2d(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamF2{t, k}, C.cam.unop(C.LcCamF2{t, k}, s)) : M.CmBlock}:
63 match s:
64 case M.CmBlock{+s0, +s1, +s2, +s3}:
65 %CoreL.u32_xor_cancel(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock}
66 %CoreL.u32_xor_cancel(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock}
67 {==}
68
69def cam_fl_step(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamFl{a, b}, C.cam.op(C.LcCamFl{a, b}, s)) : M.CmBlock}:
70 match a b s:
71 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}:
72 %cam_fl_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock}
73 %cam_flinv_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock}
74 {==}
75
76def cam_fl_step_dual(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.op(C.LcCamFl{a, b}, C.cam.unop(C.LcCamFl{a, b}, s)) : M.CmBlock}:
77 match a b s:
78 case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}:
79 %cam_flinv_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.flinv(C.cam.fl(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock}
80 %cam_fl_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock}
81 {==}
82
83def cam_unop_op(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.unop(o, C.cam.op(o, s)) : M.CmBlock}:
84 match o:
85 case C.LcCamWhite{a, b}:
86 cam_white(a, b, s)
87 case C.LcCamF1{t, k}:
88 cam_f1(t, k, s)
89 case C.LcCamF2{t, k}:
90 cam_f2(t, k, s)
91 case C.LcCamFl{a, b}:
92 cam_fl_step(a, b, s)
93 case C.LcCamSwap{}:
94 match s:
95 case M.CmBlock{s0, s1, s2, s3}:
96 {==}
97
98def cam_op_unop(o: C.LcCamOp, +s: M.CmBlock) -> {s == C.cam.op(o, C.cam.unop(o, s)) : M.CmBlock}:
99 match o:
100 case C.LcCamWhite{a, b}:
101 cam_white(a, b, s)
102 case C.LcCamF1{t, k}:
103 cam_f1d(t, k, s)
104 case C.LcCamF2{t, k}:
105 cam_f2d(t, k, s)
106 case C.LcCamFl{a, b}:
107 cam_fl_step_dual(a, b, s)
108 case C.LcCamSwap{}:
109 match s:
110 case M.CmBlock{s0, s1, s2, s3}:
111 {==}
112
113def cam_unrun_run(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.unrun(os, C.cam.run(os, s)) : M.CmBlock}:
114 match os:
115 case Nil{}:
116 {==}
117 case Con{+o, +t}:
118 %cam_unrun_run(t, C.cam.op(o, s)) : {s == C.cam.unop(o, _) : M.CmBlock}
119 cam_unop_op(o, s)
120
121def cam_run_unrun(os: List<&2, C.LcCamOp>, +s: M.CmBlock) -> {s == C.cam.run(os, C.cam.unrun(os, s)) : M.CmBlock}:
122 match os:
123 case Nil{}:
124 {==}
125 case Con{+o, +t}:
126 %cam_op_unop(o, C.cam.unrun(t, s)) : {s == C.cam.run(t, _) : M.CmBlock}
127 cam_run_unrun(t, s)
128
129def Laws.camellia_round_trip(k, b):
130 match k:
131 case C.LcCamelliaKey{ops}:
132 Equal.sym(M.CmBlock, b, C.cam.unrun(ops, C.cam.run(ops, b)), cam_unrun_run(ops, b))
133
134def Laws.camellia_round_trip_dual(k, b):
135 match k:
136 case C.LcCamelliaKey{ops}:
137 Equal.sym(M.CmBlock, b, C.cam.run(ops, C.cam.unrun(ops, b)), cam_run_unrun(ops, b))
138
139# BEGIN GENERATED by gen/vectors.py: vectors
140
141def Laws.camellia_rfc3713():
142 {==}
143
144def Laws.camellia_bad_key_length():
145 {==}
146# END GENERATED: vectors