%------------------------ Asymmetrical Encryption -------------------------

input_formula(enc_equation,axiom,(
! [E1,E2] :
( ( knows(enc(E1, E2))
  & knows(inv(E2)) )
 => knows(E1) ) )).

%---------------------- Symmetrical Encryption -----------------------------

input_formula(symenc_equation,axiom,(
! [E1,E2] :
( ( knows(symenc(E1, E2))
  & knows(E2) )
 => knows(E1) ) )).

%--------------------------- Signature -------------------------------------

input_formula(sign_equation,axiom,(
! [E,K] :
( ( knows(sign(E, inv(K) ) )
  & knows(K) )
 => knows(E) ) )).

%---- Basic Relations on Knowledge where conc, enc, symenc and sign is included ----

input_formula(construct_message_1,axiom,(
! [E1,E2] :
( ( knows(E1)
  & knows(E2) )
=> ( knows(conc(E1, E2))
   & knows(enc(E1, E2))
   & knows(symenc(E1, E2))
   & knows(dec(E1, E2))
   & knows(symdec(E1, E2))
   & knows(ext(E1, E2))
   & knows(sign(E1, E2)) ) ) )).

input_formula(construct_message_2,axiom,(
! [E1,E2] :
( ( knows(conc(E1, E2)) )
=> ( knows(E1)
  	& knows(E2) ) ) )).

%---- Basic Relations on Knowledge where head, tail and hash is included ----

input_formula(construct_message_3,axiom,(
! [E] :
( knows(E)
=> ( knows(head(E))
   & knows(tail(E))
   & knows(hash(E)) ) ) )).

%--------------------------- decryption, signature verifikation -----------------

input_formula(dec_axiom,axiom,(
! [E,K] :
( equal( dec(enc(E, K), inv(K)), E ) ) )).

input_formula(symdec_axiom,axiom,(
! [E,K] :
( equal( symdec(symenc(E, K), K), E ) ) )).

input_formula(sign_axiom,axiom,(
! [E,K] :
( equal( ext(sign(E, inv(K)), K), E ) ) )).

%--------------------------- head, tail, fst, snd, thd, frth -------------------------------------

input_formula(head_axiom,axiom,(
! [X,Y] :
( equal( head(conc(X,Y)), X ) ) )).

input_formula(tail_axiom,axiom,(
! [X,Y] :
( equal( tail(conc(X,Y)), Y ) ) )).

input_formula(fst_axiom,axiom,(
! [X] :
( equal( fst(X), head(X) ) ) )).

input_formula(snd_axiom,axiom,(
! [X] :
( equal( snd(X), head(tail(X)) ) ) )).

input_formula(thd_axiom,axiom,(
! [X] :
( equal( thd(X), head(tail(tail(X))) ) ) )).

input_formula(frth_axiom,axiom,(
! [X] :
( equal( frth(X), head(tail(tail(tail(X)))) ) ) )).

%--------------------------- mac -------------------------------------

input_formula(symmac_axiom,axiom,(
! [X,Y] :
( (knows(X) & knows(Y)) => knows(mac(X, Y)) ) )).

%----------------------- Attackers Initial Knowledge -----------------------

input_formula(previous_knowledge,axiom,(
 knows(k_ca)
 & knows(inv(k_a))
 & knows(k_a)
 )).

%----------------------- Main Protocol Specification ---------------------------

input_formula(protocol,axiom,(
 ![Init_1, Init_2, Init_3, Resp_1, Resp_2, Xchd_1] : (
 % C -> Attacker
( 
     ( ( true
       & true )
      => knows(conc( n,  conc( k_c,  sign(conc(c, conc(k_c, eol)), inv(k_c)) ) ))
     & ( ( knows(Resp_1) & knows(Resp_2)
         & equal( fst(ext(Resp_2, k_ca)), s ) & equal( snd(ext(dec(Resp_1, inv(k_c)), snd(ext(Resp_2, k_ca)))), n ) )
        => knows(symenc(secret, fst(ext(dec(Resp_1, inv(k_c)), snd(ext(Resp_2, k_ca))))))
       )
     )

)
 &  % S -> Attacker
( 
     ( ( knows(Init_1) & knows(Init_2) & knows(Init_3)
       & equal( snd(ext(Init_3, Init_2)), Init_2 ) )
      => knows(conc( enc(sign(conc(kgen(Init_2), conc(Init_1, eol)), inv(k_s)), Init_2),  sign(conc(s, conc(k_s, eol)), inv(k_ca) ) ))
     & ( ( knows(Xchd_1)
         & true )
        => true
       )
     )

)
 )  ) ).

%------------------------ Conjecture -------------------------

input_formula(attack,conjecture,(
   knows(secret) )).

% Finished