LAWS.bend

bend-osdev-camellia@0.1.0.0 · 35 lines · 4 definitions

1# Laws about Camellia (camellia.bend): for every key (every key size) and
2# block, decryption undoes encryption and encryption undoes decryption; and
3# RFC 3713's Camellia-128 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-mode-core@0.1.0.0/mode_core.bend as M
7import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
8import bend-osdev-camellia@0.1.0.0/camellia.bend as C
9
10# Camellia (RFC 3713), every key size
11
12law camellia_round_trip:
13  for k: C.LcCamelliaKey
14  for +b: M.CmBlock
15  {C.LcCamellia.decrypt(k, C.LcCamellia.encrypt(k, b)) == b : M.CmBlock}
16
17law camellia_round_trip_dual:
18  for k: C.LcCamelliaKey
19  for +b: M.CmBlock
20  {C.LcCamellia.encrypt(k, C.LcCamellia.decrypt(k, b)) == b : M.CmBlock}
21
22# Vectors: the specification's test values and refusals, proved by
23# computation (gen/vectors.py)
24
25# BEGIN GENERATED by gen/vectors.py: vectors
26# RFC 3713, Appendix A: Camellia-128, key = plaintext =
27# 0123456789ABCDEFFEDCBA9876543210, ciphertext 67673138549669730857065648EABE43
28law camellia_rfc3713:
29  {Result.map(&2, &2, L.LcError, C.LcCamelliaKey, M.CmBlock, k => C.LcCamellia.encrypt(k, M.CmBlock{19088743, 2309737967, 4275878552, 1985229328}), C.LcCamellia.key(B.Octets.of_list([1, 35, 69, 103, 137, 171, 205, 239, 254, 220, 186, 152, 118, 84, 50, 16]))) == Done{M.CmBlock{1734816056, 1419143539, 139920982, 1223343683}} : Result<&2, &2, L.LcError, M.CmBlock>}
30
31# a Camellia key of 20 bytes is refused
32law camellia_bad_key_length:
33  {Result.map(&2, &2, L.LcError, C.LcCamelliaKey, Unit, k => Unit{}, C.LcCamellia.key(B.Octets.of_list([0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]))) == Fail{L.LcBadKeyLength{20n}} : Result<&2, &2, L.LcError, Unit>}
34
35# END GENERATED: vectors