precedence([k,encrypt,tuple_4,tuple_3,'Na','Nb',decr]).
option([cnf(full),memo_constraints(on),crw_depth(1)]).

:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
begin_problem(Unknown).

list_of_descriptions.
name({*A protocol*}).
author({*Bruno Blanchet - Automatic translator*}).
status(unknown).
description({**}).
end_of_list.

list_of_symbols.
functions[(Kbs,0), (tuple_2,2), (k,3), (tuple_3,3), (tuple_4,4), 
(encrypt,2), (Kcs,0), (host,1), (Na,1), (Nb,2), (decr,1), (secretA,0), 
(secretB,0), (Kas,0)].
predicates[(c,1)].
end_of_list.
list_of_formulae(axioms).

formula(forall([any0,any1],implies(and(c(any0),c(any1)),c(tuple_2(any0,any1
))))).
formula(forall([any0,any1],implies(c(tuple_2(any0,any1)), 
and(c(any0),c(any1))))).
formula(forall([any0,any1,any2],implies(and(c(any0),c(any1),c(any2)),c(tupl
e_3(any0,any1,any2))))).
formula(forall([any0,any1,any2],implies(c(tuple_3(any0,any1,any2)), 
and(c(any0),c(any1),c(any2))))).
formula(forall([any0,any1,any2,any3],implies(and(c(any0),c(any1),c(any2),c(
any3)),c(tuple_4(any0,any1,any2,any3))))).
formula(forall([any0,any1,any2,any3],implies(c(tuple_4(any0,any1,any2,any3)
), and(c(any0),c(any1),c(any2),c(any3))))).
formula(forall([var_m,var_k], 
implies(and(c(var_k),c(encrypt(var_m,var_k))), c(var_m)))).
formula(c(host(Kas))).
formula(c(host(Kbs))).
formula(forall([var_x], implies(c(var_x), c(host(var_x))))).
formula(c(Kcs)).
formula(forall([var_y,var_x], implies(and(c(var_x),c(var_y)), 
c(encrypt(var_x,var_y))))).
formula(forall([var_x], implies(c(var_x), c(decr(var_x))))).
formula(forall([var_x], implies(c(decr(var_x)), c(var_x)))).
formula(forall([var_h], implies(c(var_h), 
c(tuple_3(host(Kas),var_h,Na(var_h)))))).
formula(forall([var_m,var_key,var_h], 
implies(c(encrypt(tuple_4(Na(var_h),var_h,var_key,var_m),Kas)), 
c(var_m)))).
formula(forall([var_m,var_n,var_key,var_h], 
implies(and(c(encrypt(tuple_4(Na(var_h),var_h,var_key,var_m),Kas)),c(encryp
t(var_n,var_key))), c(encrypt(decr(var_n),var_key))))).
formula(forall([var_m,var_key], 
implies(c(encrypt(tuple_4(Na(host(Kbs)),host(Kbs),var_key,var_m),Kas)), 
c(encrypt(secretA,var_key))))).
formula(forall([var_h,var_key], 
implies(c(encrypt(tuple_2(var_key,var_h),Kbs)), 
c(encrypt(Nb(var_key,var_h),var_key))))).
formula(forall([var_key], 
implies(and(c(encrypt(tuple_2(var_key,host(Kas)),Kbs)),c(encrypt(decr(Nb(va
r_key,host(Kas))),var_key))), c(encrypt(secretB,var_key))))).
formula(forall([var_n,var_Ks2,var_Ks1], 
implies(c(tuple_3(host(var_Ks1),host(var_Ks2),var_n)), 
c(encrypt(tuple_4(var_n,host(var_Ks2),k(var_Ks1,var_Ks2,var_n),encrypt(tupl
e_2(k(var_Ks1,var_Ks2,var_n),host(var_Ks1)),var_Ks2)),var_Ks1))))).

end_of_list.

list_of_formulae(conjectures).

formula(c(secretB)).
formula(c(secretA)).

end_of_list.

end_problem.

/*

Saturation terminated.

Persisting Clauses:

    1(1) : c(B),c(C) -> c(tuple_2(B,C))
    7(1) : c(encrypt(B,C)),c(C) -> c(B)
    8(1) : c(host(Kas))
    9(1) : c(host(Kbs))
   10(1) : c(B) -> c(host(B))
   11(1) : c(Kcs)
   12(1) : c(B),c(C) -> c(encrypt(B,C))
   13(1) : c(B) -> c(decr(B))
   14(1) : c(decr(B)) -> c(B)
   15(1) : c(B) -> c(tuple_3(host(Kas),B,Na(B)))
   16(1) : c(encrypt(tuple_4(Na(B),B,C,D),Kas)) -> c(D)
   17(1) : c(encrypt(tuple_4(Na(B),B,C,D),Kas)),c(encrypt(E,C)) -> c(encrypt(decr(E),C))
   18(1) : c(encrypt(tuple_4(Na(host(Kbs)),host(Kbs),B,C),Kas)) -> c(encrypt(secretA,B))
   19(1) : c(encrypt(tuple_2(B,C),Kbs)) -> c(encrypt(Nb(B,C),B))
   20(1) : c(encrypt(tuple_2(B,host(Kas)),Kbs)),c(encrypt(decr(Nb(B,host(Kas))),B)) -> c(encrypt(secretB,B))
   21(1) : c(tuple_3(host(B),host(C),D)) -> c(encrypt(tuple_4(D,host(C),k(B,C,D),encrypt(tuple_2(k(B,C,D),host(B)),C)),B))
   22(1) + c(secretB) -> 
   23(1) + c(secretA) -> 
   24(2) : c(B),c(C),c(D) -> c(tuple_3(D,B,C))
   25(2) : c(B),c(C),c(D),c(E) -> c(tuple_4(E,D,B,C))
   26(2) : c(tuple_2(B,C)) -> c(B)
   27(2) : c(tuple_2(B,C)) -> c(C)
   28(2) : c(tuple_3(B,C,D)) -> c(B)
   30(2) : c(tuple_4(B,C,D,E)) -> c(B)
   38(2) : c(B),c(tuple_3(host(B),host(C),D)) -> c(tuple_4(D,host(C),k(B,C,D),encrypt(tuple_2(k(B,C,D),host(B)),C)))
   39(2) : c(tuple_3(host(Kas),host(B),Na(host(B)))) -> c(encrypt(tuple_2(k(Kas,B,Na(host(B))),host(Kas)),B))
   41(2) : c(tuple_3(host(Kas),host(B),Na(host(B)))),c(encrypt(C,k(Kas,B,Na(host(B))))) -> c(encrypt(decr(C),k(Kas,B,Na(host(B)))))
   43(3) : c(encrypt(secretA,k(Kas,Kbs,Na(host(Kbs)))))
   44(3) : c(tuple_3(B,C,D)) -> c(C)
   45(3) : c(tuple_3(B,C,D)) -> c(D)
   46(3) : c(tuple_4(B,C,D,E)) -> c(C)
   58(5) + c(k(Kas,Kbs,Na(host(Kbs)))) -> 
   68(4) : c(tuple_4(B,C,D,E)) -> c(D)
   69(4) : c(tuple_4(B,C,D,E)) -> c(E)
   70(4) : c(B) -> c(Na(B))
   89(8) + c(Kas) -> 
   91(5) : c(B) -> c(tuple_2(k(Kas,B,Na(host(B))),host(Kas)))
   92(5) : c(encrypt(Nb(k(Kas,Kbs,Na(host(Kbs))),host(Kas)),k(Kas,Kbs,Na(host(Kbs)))))
   93(6) : c(encrypt(secretB,k(Kas,Kbs,Na(host(Kbs)))))
   97(5) : c(B),c(tuple_3(host(B),host(C),D)) -> c(k(B,C,D))
   98(5) : c(B),c(tuple_3(host(B),host(C),D)) -> c(encrypt(tuple_2(k(B,C,D),host(B)),C))
  101(6) : c(B) -> c(k(Kas,B,Na(host(B))))
 106(11) + c(Kbs) -> 
  110(6) : c(B),c(tuple_3(host(B),host(Kbs),C)) -> c(encrypt(Nb(k(B,Kbs,C),host(B)),k(B,Kbs,C)))
  114(8) : c(B),c(tuple_3(host(B),host(Kbs),C)) -> c(Nb(k(B,Kbs,C),host(B)))



Total time: 1963553 milliseconds

Number of forward inferences: 53
Number of tableau inferences: 12
Number of generated clauses: 114
Number of kept clauses: 67
yes

*/