LAWS.bend

bend-osdev-blowfish@0.1.0.0 · 29 lines · 3 definitions

1# Laws about Blowfish (blowfish.bend): for every key and block, decryption
2# undoes encryption and encryption undoes decryption; and a refused key,
3# 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-blowfish@0.1.0.0/blowfish.bend as BF
8
9# Blowfish (Schneier), every key
10
11law blowfish_round_trip:
12  for k: BF.LcBlowfishKey
13  for +b: L.LcBlock64
14  {BF.LcBlowfish.decrypt(k, BF.LcBlowfish.encrypt(k, b)) == b : L.LcBlock64}
15
16law blowfish_round_trip_dual:
17  for k: BF.LcBlowfishKey
18  for +b: L.LcBlock64
19  {BF.LcBlowfish.encrypt(k, BF.LcBlowfish.decrypt(k, b)) == b : L.LcBlock64}
20
21# A refusal, proved by computation (gen/vectors.py); Schneier's vectors run
22# in check.bend (README.md, Laws)
23
24# BEGIN GENERATED by gen/vectors.py: vectors
25# a Blowfish key of 3 bytes is refused (32 bits at least)
26law blowfish_bad_key_length:
27  {Result.map(&2, &2, L.LcError, BF.LcBlowfishKey, Unit, k => Unit{}, BF.LcBlowfish.key(B.Octets.of_list([0, 0, 0]))) == Fail{L.LcBadKeyLength{3n}} : Result<&2, &2, L.LcError, Unit>}
28
29# END GENERATED: vectors