law aesround_rfc10032

bend-osdev-aead@0.1.0.0 · LAWS.bend:54

import bend-osdev-aead@0.1.0.0/LAWS.bend as LAWS
import Base
import bend-osdev-aead@0.1.0.0/aesround.bend as R

54# RFC 10032, Appendix A.1: AESRound(000102..0f, 101112..1f) =
55# 7a7b4e5638782546a8c0477a3b813f43
56law aesround_rfc10032:
57  {R.AdAes.round(R.AdAes.sbox(), R.AdBlk{66051, 67438087, 134810123, 202182159}, R.AdBlk{269554195, 336926231, 404298267, 471670303}) == R.AdBlk{2054901334, 947397958, 2831173498, 998326083} : R.AdBlk}

Uses (3)

Used by (0)

No other definition uses this definition.