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})
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})