PROOF.bend

bend-osdev-cast5@0.1.0.0 · 35 lines · 0 definitions

1import Base
2import bend-osdev-bytes@0.1.1.0/bytes.bend as B
3import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
4import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
5import bend-osdev-cipher-core@0.1.0.0/PROOF.bend as CoreP
6import bend-osdev-cast5@0.1.0.0/cast5.bend as C5
7import bend-osdev-cast5@0.1.0.0/LAWS.bend as Laws
8
9def swap2(b: L.LcBlock64) -> {b == L.lc.swap(L.lc.swap(b)) : L.LcBlock64}:
10  match b:
11    case L.LcBlock64{h, l}:
12      {==}
13
14# CAST-128: its rounds, then the exchange of the halves, undone
15
16def Laws.cast5_round_trip(k, b):
17  match k:
18    case C5.LcCast5Key{+rks}:
19      %swap2(L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)) : {L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, _) == b : L.LcBlock64}
20      Equal.sym(L.LcBlock64, b, L.lc.fe.unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.fe.run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b)), CoreL.feistel_unrun_run(~C5.LcCast5Rk, ~C5.cast5.f, rks, b))
21
22def Laws.cast5_round_trip_dual(k, b):
23  match k:
24    case C5.LcCast5Key{+rks}:
25      %CoreL.feistel_run_unrun(~C5.LcCast5Rk, ~C5.cast5.f, rks, L.lc.swap(b)) : {L.lc.swap(_) == b : L.LcBlock64}
26      Equal.sym(L.LcBlock64, b, L.lc.swap(L.lc.swap(b)), swap2(b))
27
28# BEGIN GENERATED by gen/vectors.py: vectors
29
30def Laws.cast5_rfc2144():
31  {==}
32
33def Laws.cast5_bad_key_length():
34  {==}
35# END GENERATED: vectors