LAWS.bend

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

1# Laws about CAST-128 (cast5.bend): for every key (every key size) and
2# block, decryption undoes encryption and encryption undoes decryption; and
3# RFC 2144 B.1's 128-bit vector and a refused key, proved by computation.
4import Base
5import bend-osdev-bytes@0.1.1.0/bytes.bend as B
6import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
7import bend-osdev-cast5@0.1.0.0/cast5.bend as C5
8
9# CAST-128 (RFC 2144), every key size
10
11law cast5_round_trip:
12  for k: C5.LcCast5Key
13  for +b: L.LcBlock64
14  {C5.LcCast5.decrypt(k, C5.LcCast5.encrypt(k, b)) == b : L.LcBlock64}
15
16law cast5_round_trip_dual:
17  for k: C5.LcCast5Key
18  for +b: L.LcBlock64
19  {C5.LcCast5.encrypt(k, C5.LcCast5.decrypt(k, b)) == b : L.LcBlock64}
20
21# Vectors: the specification's test values and refusals, proved by
22# computation (gen/vectors.py)
23
24# BEGIN GENERATED by gen/vectors.py: vectors
25# RFC 2144, Appendix B.1: CAST-128 with the 128-bit key
26# 0123456712345678234567893456789A, plaintext 0123456789ABCDEF, ciphertext
27# 238B4FE5847E44B2
28law cast5_rfc2144:
29  {Result.map(&2, &2, L.LcError, C5.LcCast5Key, L.LcBlock64, k => C5.LcCast5.encrypt(k, L.LcBlock64{19088743, 2309737967}), C5.LcCast5.key(B.Octets.of_list([1, 35, 69, 103, 18, 52, 86, 120, 35, 69, 103, 137, 52, 86, 120, 154]))) == Done{L.LcBlock64{596332517, 2222867634}} : Result<&2, &2, L.LcError, L.LcBlock64>}
30
31# a CAST-128 key of 4 bytes is refused (40 bits at least)
32law cast5_bad_key_length:
33  {Result.map(&2, &2, L.LcError, C5.LcCast5Key, Unit, k => Unit{}, C5.LcCast5.key(B.Octets.of_list([0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{4n}} : Result<&2, &2, L.LcError, Unit>}
34
35# END GENERATED: vectors