Section 2: Prince is essentially a 64-bit cipher, with 128-bit key, coming in two parts.

Plantext is simply a block.

Key is again a 64-bit block.

Cypher text is another 64-bit block.

A nibble is 4-bits. Ideally, we would like to represent a nibble by SWord 4; and indeed SBV can do that for verification purposes just fine. Unfortunately, the SBV's C compiler doesn't support 4-bit bit-vectors, as there's nothing meaningful in the C-land that we can map it to. Thus, we represent a nibble with 8-bits. The top 4 bits will always be 0.

Expanding a key, from Section 3.4 of the spec.

expandKey(x) = x has a unique solution. We have:

>>> prop_ExpandKey
Q.E.D.

Section 2: Encryption

Decryption

Basic prince algorithm

Core prince. It's essentially folding of 12 rounds stitched together:

Forward round.

Backend round.

M transformation.

Inverse of M.

SR.

Inverse of SR:

Prove sr and srInv are inverses: We have:

>>> prove prop_sr
Q.E.D.

M' transformation

The matrix as described in Section 3.3

Multiplication.

Non-linear transformation of a block

SBox transformation.

Inverse SBox transformation.

Prove that sbox and sBoxInv are inverses: We have:

>>> prove prop_SBox
Q.E.D.

Round constants

Round-constants property: rc_i xor rc_{11-i} is constant. We have:

>>> prop_RoundKeys
True

Convert a 64 bit word to nibbles

Convert from nibbles to a 64 bit word

From Appendix A of the spec. We have:

>>> testVectors
True

Nicely show a concrete block.

Generating C code for the encryption block.