securityauthenticationencryptionencryption-symmetric

Invalid expression to be encrypted in SPAN AVISPA


Can someone corrected me on what did i do wrong in line 15? It produced:

%% Syntax error: Line 15, Col 42 (offset 538-538, string ")")
%% Syn.Err(901): invalid expression to be encrypted

And the code for Line 15 is:

State = 1 /\ Rcv({Di'.Ei'.Fi',N'}_SKey2) =|> State' = 2 /\ Ci' = exp(IDi, Ai) /\ Bi' = xor(Di',Ci') 
/\ Ri' = new() /\ M1' =h(Bi'.Ri') /\ M2' = xor(h(Bi'), Ri') /\ Snd(M1'.M2'.Fi.IDj) /\ secret({PW1}, 
sec1, {Ui})

Solution

  • State = 1 /\ Rcv({Di'.Ei'.Fi',N'}_SKey2) =|> State' = 2 /\ Ci' = exp(IDi, Ai) /\ Bi' = xor(Di',Ci') /\ Ri' := new() /\ M1' =h(Bi'.Ri') /\ M2' = xor(h(Bi'), Ri') /\ Snd(M1'.M2'.Fi.IDj) /\ secret({PW1}, sec1, {Ui})