(* This file gives the definition of CSS as a relation. *) Module cssrel Import sector misc arith trich indrel ; (* The map from L to Lprime *) [ Lprime = [w:word] wXor w (wSHR14 w) ]; (* The map from M to Mprime *) [ Mprime = [w:word] wXor w ( wXor (wSHR3 w) ( wXor (wSHR4 w) (wSHR12 w))) ]; (***** We put a Key and Sector into the environment. We don't generalise on these until the file cssexist.l *****) (* The key bytes *) [ K0, K1, K2, K3, K4 : byte ]; (* The input sector *) [ S : sector ]; (* The modified key *) [ Kprime0 = byteToWord (reverse (bXor K0 (S num84 index84))) ]; [ Kprime1 = byteToWord (reverse (bXor K1 (S num85 index85))) ]; [ Kprime2 = byteToWord (reverse (bXor K2 (S num86 index86))) ]; [ Kprime3 = byteToWord (reverse (bXor K3 (S num87 index87))) ]; [ Kprime4 = byteToWord (reverse (bXor K4 (S num88 index88))) ]; (***** L *****) (* The L127 constant. *) [ L127 = wOr Kprime1 (wOr wExp8 (wSHL9 Kprime0)) ]; (* The step function in the defining condition for L *) [ Lstep = [w:word] wXor (wSHR8 w) ( wXor (wSHL9 (Lprime w)) ( wXor (wSHL12 (Lprime w)) (wSHL15 (Lprime w)))) ]; (* LpredRaw: The guts of predicate that defines the L relation *) [ LpredRaw = [L:nat->word->Prop][i:nat][w:word] ( (is127 i) -> Eq w L127 ) /\ ( (in128to2048 i) -> Ex[ww : word] (L (pred i) ww) /\ Eq w (Lstep ww) ) ]; (* L is now defined as a fix point *) [ L = Fix LpredRaw ]; (* The predicate that says that L has an output for every input. Note that this is slightly stronger than the obvious statement. *) [ Lexist = {i:nat} (in128to2048 i) -> Ex[w:word] L i w ]; (***** M *****) (* The M127 constant *) [ M127 = wOr Kprime4 ( wOr (wSHL8 (Kprime3)) ( wOr (wSHL16 (wAnd Kprime2 w00011111)) ( wOr wExp21 ( wSHL17 (wAnd Kprime2 w11100000))))) ]; (* The step function in the defining condition for M *) [ Mstep = [w:word] wXor (wSHR8 w) (wSHL17 w) ]; (* MpredRaw: The guts of predicate that defines the M relation *) [ MpredRaw = [M:nat->word->Prop][i:nat][w:word] ( (is127 i) -> Eq w M127) /\ ( (in128to2048 i) -> Ex[ww : word] (M (pred i) ww) /\ Eq w (Mstep ww) ) ]; (* M is now defined as a fix point *) [ M = Fix MpredRaw ]; (* The predicate that says that M has an output for every input. *) [ Mexist = {i:nat} (in128to2048 i) -> Ex[w:word] M i w ]; (***** X *****) [ Xstep = [l,m:word][w:word] wSum (wAnd w11111111 (wNot (wSHR9 l))) ( wSum (wSHR17 m) (wSHR8 w)) ]; [ XpredRaw = [X:nat->word->Prop][i:nat][w:word] ( (is127 i) -> Eq w wZero ) /\ ( (in128to2048 i) -> Ex3[ww, l, m : word] (X (pred i) ww) /\ (L i l) /\ (M i m) /\ Eq w (Xstep l m ww)) ]; (* X is defined as a fix point *) [ X = Fix XpredRaw ]; (* The predicate that says that X has an output for every input. Note that this is slightly stronger than the obvious statement. *) [ Xexist = {i:nat} (in128to2048 i) -> Ex[w:word] X i w ]; (***** The CSS predicate *****) [ CSS = [i:nat][ii:index i][b:byte] ((lt127 i) -> Eq b (S i ii)) /\ ((is127 i) -> Eq b (S i ii)) /\ ((in128to2048 i) -> Ex[ww:word] (X i ww) /\ Eq b (bXor (wLowByte ww) (PAL (S i ii)))) ];