?prevdifflink? - Blame
values
Word_Length = 32;
Maximum_Number_Size = 2 ** Word_Length - 1;
Maximum_Number_Size_plus_1 = Maximum_Number_Size + 1;
Maximum_Number_Size_plus_1_div_2 = Maximum_Number_Size_plus_1 div 2;
Maximum_No_of_Message_blocks = 1000000;
A = 2 * 2 **24 + 4 * 2 **16 + 8 * 2 **8 + 1;
B = 0 * 2 **24 + 128 * 2 **16 + 64 * 2 **8 + 33;
C = 191 * 2 **24 + 239 * 2 **16 + 127 * 2 **8 + 223;
D = 125 * 2 **24 + 254 * 2 **16 + 251 * 2 **8 + 255;
Maximum_No_of_blocks_for_MAC = 1024 div 4;
Maximum_No_of_blocks_for_MAC_plus_1 = Maximum_No_of_blocks_for_MAC + 1
types
Number = nat
inv N == N < Maximum_Number_Size_plus_1;
Bit = nat
inv B == B in set {0,1};
Message_in_bits = seq of Bit
inv M ==
if len M mod Word_Length = 0
then ( len M div Word_Length <= Maximum_No_of_Message_blocks) and
( len M > 0)
else len M div Word_Length + 1 <= Maximum_No_of_Message_blocks;
Message_in_blocks_plus_empty_Message = seq of Number
inv M == len M <= Maximum_No_of_Message_blocks;
Message_in_blocks = Message_in_blocks_plus_empty_Message
inv M == 1 <= len M;
Double_Number = seq of Number
inv D == len D = 2;
Key = Double_Number;
Key_Constant :: X0 : Number
Y0 : Number
V0 : Number
W : Number
S : Number
T : Number
functions
Pad_out_Message: Message_in_bits -> Message_in_bits
Pad_out_Message(M) ==
let No_Extra_bits = Word_Length - len M mod Word_Length in
if No_Extra_bits = Word_Length
then M
else M ^ Get_Application_defined_bits(M,No_Extra_bits);
Get_Application_defined_bits(M: Message_in_bits, No_bits: nat)
Extra : Message_in_bits
pre No_bits < Word_Length
post len Extra = No_bits;
Form_Message_into_blocks: Message_in_bits -> Message_in_blocks
Form_Message_into_blocks(M) ==
if len M = Word_Length
then [Form_Number(M)]
else [Form_Number(Get_head_in_bits(M,Word_Length))] ^
Form_Message_into_blocks(Get_tail_in_bits(M,Word_Length))
pre ( len M >= Word_Length) and ( len M mod Word_Length = 0);
Form_Number: Message_in_bits -> Number
Form_Number(M) ==
if len M = 1 then hd M
else hd M + 2 * Form_Number( tl M)
pre len M <= Word_Length;
CYC: Number -> Number
CYC(X) ==
ADD(X,X) + CAR(X,X);
AND: Number * Number -> Number
AND(X,Y) ==
if (X = 0) or (Y = 0)
then 0
else (X mod 2) * (Y mod 2) + 2 * AND(X div 2,Y div 2);
OR: Number * Number -> Number
OR(X,Y) ==
if (X = 0) or (Y = 0)
then X + Y
else max(X mod 2,Y mod 2) + 2 * OR(X div 2,Y div 2);
max: int * int -> int
max(X,Y) ==
if X >= Y
then X
else Y;
XOR: Number * Number -> Number
XOR(X,Y) ==
if (X = 0) or (Y = 0)
then X + Y
else (X + Y) mod 2 + 2 * XOR(X div 2,Y div 2);
ADD: Number * Number -> Number
ADD(X,Y) ==
(X + Y) mod Maximum_Number_Size_plus_1;
CAR: Number * Number -> Number
CAR(X,Y) ==
(X + Y) div Maximum_Number_Size_plus_1;
MUL1: Number * Number -> Number
MUL1(X,Y) ==
let L = (X * Y) mod Maximum_Number_Size_plus_1,
U = (X * Y) div Maximum_Number_Size_plus_1 in
let S = ADD(U,L),
C = CAR(U,L) in ADD(S,C);
MUL2: Number * Number -> Number
MUL2(X,Y) == let L = (X * Y) mod Maximum_Number_Size_plus_1,
U = (X * Y) div Maximum_Number_Size_plus_1 in let D = ADD(U,U),
E = CAR(U,U) in let F = ADD(D,2 * E) in let S = ADD(F,L),
C = CAR(F,L) in ADD(S,2 * C);
MUL2A: Number * Number -> Number
MUL2A(X,Y) ==
let L = (X * Y) mod Maximum_Number_Size_plus_1,
U = (X * Y) div Maximum_Number_Size_plus_1 in
let D = ADD(U,U) in
let S = ADD(D,L),
C = CAR(D,L) in ADD(S,2 * C)
pre (X div Maximum_Number_Size_plus_1_div_2 = 0) or
(Y div Maximum_Number_Size_plus_1_div_2 = 0);
BYT: Double_Number -> Double_Number
BYT(K) ==
let X = hd K,
Y = hd tl K in
let X` = [Byte(X,3),Byte(X,2),Byte(X,1),Byte(X,0)],
Y` = [Byte(Y,3),Byte(Y,2),Byte(Y,1),Byte(X,0)] in
let XY = X` ^ Y`,
P = 0 in
let XY` = Condition_Sequence(XY,P) in
let X`` = Get_head_in_blocks(XY`,4),
Y`` = Get_tail_in_blocks(XY`,4) in
[Convert_Bytes_to_Number(X``)] ^ [Convert_Bytes_to_Number(Y``)];
Byte: Number * nat -> Number
Byte(N,B) ==
if B = 0
then N mod 2 **8
else Byte(N div 2 **8,B - 1)
pre (B >= 0) and (B <= 3);
Condition_Sequence: Message_in_blocks * Number -> Message_in_blocks
Condition_Sequence(M,P) ==
if len M = 1
then [Condition_value( hd M,P)]
else [Condition_value( hd M,P)] ^
Condition_Sequence( tl M,Changes( hd M,P));
Condition_value: Number * Number -> Number
Condition_value(B,P) ==
let P` = 2 * P in
let P`` = P` + 1 in
if B = 0 then P``
else if B = 2 **8 - 1
then 2 **8 - 1 - P``
else B;
Changes: Number * Number -> Number
Changes(B,P) ==
let P` = 2 * P in
let P`` = P` + 1 in
if (B = 0) or (B = 2 **8 - 1)
then P``
else P`;
Convert_Bytes_to_Number: Message_in_blocks -> Number
Convert_Bytes_to_Number(M) ==
if len M = 1
then hd M
else Convert_Bytes_to_Number( tl M) + hd M * 2 **(8 * ( len M - 1));
PAT: Double_Number -> Number
PAT(D) ==
let X = hd D,
Y = hd tl D in
let X` = [Byte(X,3),Byte(X,2),Byte(Y,1),Byte(Y,0)],
Y` = [Byte(Y,3),Byte(Y,2),Byte(Y,1),Byte(Y,0)] in
let XY = X` ^ Y`,
P = 0 in
Record_Changes(XY,P);
Record_Changes: Message_in_blocks * Number -> Number
Record_Changes(M,P) ==
if len M = 1
then Changes( hd M,P)
else Record_Changes( tl M,Changes( hd M,P));
Prelude: Key -> Key_Constant
Prelude(K) ==
let J1K1 = BYT(K) in
let J1 = hd J1K1,
K1 = hd tl J1K1,
P = PAT(K),
Q = (1 + P) * (1 + P) in
let J12 = MUL1(J1,J1),
J22 = MUL2(J1,J1) in
let J14 = MUL1(J12,J12),
J24 = MUL2(J22,J22) in
let J16 = MUL1(J12,J14),
J26 = MUL2(J22,J24) in
let J18 = MUL1(J12,J16),
J28 = MUL2(J22,J26) in
let H4 = XOR(J14,J28),
H6 = XOR(J16,J26),
H8 = XOR(J18,J28) in
let K12 = MUL1(K1,K1),
K22 = MUL2(K1,K1) in
let K14 = MUL1(K12,K12),
K24 = MUL2(K22,K22) in
let K15 = MUL1(K1,K14),
K25 = MUL2(K1,K24) in
let K17 = MUL1(K12,K15),
K27 = MUL2(K22,K25) in
let K19 = MUL1(K12,K17),
K29 = MUL2(K22,K27) in
let H` = XOR(K15,K25) in
let H5 = MUL2(H`,Q),
H7 = XOR(K17,K27),
H9 = XOR(K19,K29) in
let X0Y0 = BYT([H4,H5]),
V0W = BYT([H6,H7]),
ST = BYT([H8,H9]) in
mk_Key_Constant( hd X0Y0, hd tl X0Y0, hd V0W, hd tl V0W, hd ST, hd tl ST);
Main_loop: Message_in_blocks_plus_empty_Message * Key_Constant -> Number
Main_loop(M,KC) ==
let mk_Key_Constant(X,Y,V,W,S,T) = KC in
if len M = 0
then XOR(X,Y)
else let Mi = hd M in
let V` = CYC(V) in
let E = XOR(V`,W),
X` = XOR(X,Mi),
Y` = XOR(Y,Mi) in
let F = ADD(E,Y`),
G = ADD(E,X`) in
let F` = OR(F,A),
G` = OR(G,B) in
let F`` = AND(F`,C),
G`` = AND(G`,D) in
let X`` = MUL1(X`,F``),
Y`` = MUL2A(Y`,G``) in
Main_loop( tl M,mk_Key_Constant(X``,Y``,V`,W,S,T));
Z: Message_in_blocks * Key -> Number
Z(M,K) ==
let KC = Prelude(K) in
let S = KC.S,
T = KC.T in
let M` = M ^ [S] ^ [T] in
Main_loop(M`,KC);
MAC: Message_in_bits * Key -> Number
MAC(M,K) ==
let M` = Pad_out_Message(M) in
let M`` = Form_Message_into_blocks(M`) in
if len M`` <= Maximum_No_of_blocks_for_MAC
then Z(M``,K)
else let M``` =
[Z(Get_head_in_blocks(M``,Maximum_No_of_blocks_for_MAC),K)]
^ Get_tail_in_blocks(M``,Maximum_No_of_blocks_for_MAC) in
Z_of_SEG(M```,K,Maximum_No_of_blocks_for_MAC_plus_1);
Z_of_SEG: Message_in_blocks * Key * nat -> Number
Z_of_SEG(M,K,No_blocks) ==
if len M <= No_blocks
then Z(M,K)
else let M` = [Z(Get_head_in_blocks(M,No_blocks),K)] ^
Get_tail_in_blocks(M,No_blocks) in
Z_of_SEG(M`,K,No_blocks);
Get_tail_in_bits: Message_in_bits * nat -> Message_in_bits
Get_tail_in_bits(M,No_bits) ==
if No_bits = 0
then M
else Get_tail_in_bits( tl M,No_bits - 1)
pre len M >= No_bits;
Get_head_in_bits: Message_in_bits * nat -> Message_in_bits
Get_head_in_bits(M,No_bits) ==
if No_bits = 0
then [ hd M]
else [ hd M] ^ Get_head_in_bits( tl M,No_bits - 1)
pre ( len M >= No_bits) and (No_bits >= 1);
Get_tail_in_blocks: Message_in_blocks * nat -> Message_in_blocks
Get_tail_in_blocks(M,No_blocks) ==
if No_blocks = 0
then M
else Get_tail_in_blocks( tl M,No_blocks - 1)
pre len M >= No_blocks;
Get_head_in_blocks: Message_in_blocks * nat -> Message_in_blocks
Get_head_in_blocks(M,No_blocks) ==
if No_blocks = 0
then [ hd M]
else [ hd M] ^ Get_head_in_blocks( tl M,No_blocks - 1)
pre ( len M >= No_blocks) and (No_blocks >= 1)
|