LAWS.bend

bend-osdev-aria@0.1.0.0 · 36 lines · 0 definitions

1# Laws about ARIA (aria.bend): for every key (every key size) and block,
2# decryption undoes encryption and encryption undoes decryption; and RFC
3# 5794 A.1 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-aria@0.1.0.0/aria.bend as A
9
10# ARIA (RFC 5794), every key size
11
12law aria_round_trip:
13  for k: A.LcAriaKey
14  for +b: M.CmBlock
15  {A.LcAria.decrypt(k, A.LcAria.encrypt(k, b)) == b : M.CmBlock}
16
17law aria_round_trip_dual:
18  for k: A.LcAriaKey
19  for +b: M.CmBlock
20  {A.LcAria.encrypt(k, A.LcAria.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 5794, Appendix A.1: ARIA-128, key 000102030405060708090A0B0C0D0E0F,
27# plaintext 00112233445566778899AABBCCDDEEFF, ciphertext
28# D718FBD6AB644C739DA95F3BE6451778
29law aria_rfc5794:
30  {Result.map(&2, &2, L.LcError, A.LcAriaKey, M.CmBlock, k => A.LcAria.encrypt(k, M.CmBlock{1122867, 1146447479, 2291772091, 3437096703}), A.LcAria.key(B.Octets.of_list([0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]))) == Done{M.CmBlock{3608738774, 2875477107, 2645122875, 3863287672}} : Result<&2, &2, L.LcError, M.CmBlock>}
31
32# an ARIA key of 20 bytes is refused
33law aria_bad_key_length:
34  {Result.map(&2, &2, L.LcError, A.LcAriaKey, Unit, k => Unit{}, A.LcAria.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>}
35
36# END GENERATED: vectors