光阴冢

We make choices and life has a way of making us pay for them.

AES Specification

Jul 30, 2020  

How to prove the finite property for the type GF2pow8

  1. Prove that for a fixed n, GF2powN is finite by induction on the degree.
    1. Case 0, trivial.
    2. Case (Suc N).
      1. Case (Suc 0), trivial.
      2. Case (Suc (Suc M)), the set can be generated from the degree (Suc M).
  2. Automatically for case 8, the set is finite.

How to implement the inverse using the extended Euclidean algorithm

  1. Refer to the bezw term.
  2. Using a new user-defined induct rule:
    • Assumes \(\bigwedge m.~P~m~0\) and \(\bigwedge m.~P~m~1\) and \(\bigwedge m~n.~0 ≠ n ⟹ 1 ≠ n ⟹ P~n (m \mod n) ⟹ P ~m~n\)
    • Shows \(P~m~n\)

How to prove the irreduciblity?

  1. Basic idea, by brute force all the polys whose degrees less that 9.
    1. Also a new induct rule?
    2. How to apply the calculation process?
  2. Prove each degree seperately, along with some obvious lemmas. (For example, degree (8 - m) and degree m can be taken together.)
  3. Maybe there is no automatic way to prove this. (What if the degree is larger?)

How to model the representations?

Like bit lists, natural numbers range from 0–256.

Use bin_to_bl and bl_to_bin functions to convert between naturals and \(\text{GF}_2^8\). But be cautious about the sequence of the bits in this representation. It may be reversed.

About the computation of the conversion between numbers and \(\text{GF}_2^8\) elements, we will talk about it in the Code Generation Part.

Failed attempts:

  1. To instantiate the countable class: it provides from_nat and to_nat functions, but it seems that the constants related lemma can’t be proved by simply applying eval(some basic problems with the code gen part).
  2. To instantiate the numeral class: it will comprehend terms like 0x08 as \(\text{GF}_2^8\) type, but in an “add-one” way, thus the results can be only 1 or zero since add is actually binary XOR.

How to formalize the computation between the matrices?

Using Jordan_Normal_Form.Matrix from AFP for now.

Use HOL-Analysis.Finite_Cartesian_Product. Build the matrices from vectors, and build the vectors from vec_lambda constructor.

Implement the numeral type four to formalize the index of the matrices.

We can just use the numeral type predefined in theory HOL-Library.Numeral_Type. More concretly, use HOL-Library.Typed_length.

About the computations, this theory provides many useful functions:

  1. map_matrix
  2. the inherited plus, multiply or something else.

Proofs about the Cipher itself

  1. Round Ops can be inversed.

    1. SubBytes, skipped for now, it is also related to the codegen part.
    2. MixColumns, assert that the used two matrices are indeed inversed to each other. (This assertion need to be proved further).
    3. ShiftRows. The \((+1)\) operation for numeral types can help.
    4. AddRoundKey. The add for \(\text{GF}_2^8\) is actually XOR. Thus this can be proved simply.
  2. Ciphers that using these Round Ops

    1. The key_schedule part is straight-forward. (\( \forall k, f(k) = f(k) \))
    2. Unfolding all the definitions and former lemmas.

Code Generation

Three problems. (Comments from Albert)

  1. No constructor for the type ('a, 'b) vec

    Note that vec is a typedef-ed type and it usually means that the code generation technology does not know how to represent this in code. Luckily, we can simply solve this problem by declaring vec_lambda as the code_datatype and vec_lambda_beta as a code equation (for evaluating vec_nth).

  2. Handling UNIV set in code

    We still have problem with the code representation of UNIV. If you type code_thms "(**)" you will see that matrix-matrix multiplication involves the UNIV set and its representation is UNIV = List.coset []. If you access the element of matrix-matrix multiplication via vec_nth, you will have a Match exception raised.

  3. Matrix equality in code

    Previous solutions still would not allow you to evaluate whether two matrices are equal or not. If you try it immediately, it will keep (possibly) forever. The culprit is the equality definition of two matrices: two matrices are equal if their function representation is equal. This means that you have to evaluate for all domain that two functions are equal f1 = f2 <-> ∀x. f1 x = f2 x and our domain here is unfortunately naturals. But we don’t actually have to do that if we monomorphise our matrices equality to GF2pow8^4^4; we only need to check for set [0, 1, 2, 3] or any four consecutive numbers.

What’s more, I need to read the related Isabelle refs to get a better understanding of codegen.

Lessons

  1. Use predefined lemmas and functions as much as possible. (use find_consts and find_theorems)
  2. Tear the big problems apart into very very small pieces.
  3. Use class based other than locale based when possible.

(T.B.A)