use(exp).

attacker(tuple_base).
attacker(B),attacker(C) -> attacker(tuple_2(B,C)).
attacker(tuple_2(B,C)) => attacker(B)and attacker(C).
attacker(B), attacker(C), attacker(D) -> attacker(tuple_3(B,C,D)).
attacker(tuple_3(B,C,D)) => attacker(B)and(attacker(C)and attacker(D)).
attacker(B),attacker(C),attacker(D),attacker(E) -> attacker(tuple_4(B,C,D,E)).
attacker(tuple_4(B,C,D,E)) => attacker(B)and(attacker(C)and(attacker(D)and attacker(E))).
attacker(sencrypt(B,C)),attacker(C) -> attacker(B).
attacker(B) -> attacker(hash(B)).
attacker(B),attacker(C) -> attacker(encrypt(B,C)).
attacker(B),attacker(C) -> attacker(keyhash(B,C)).
attacker(B) -> attacker(pk(B)).
attacker(encrypt(B,pk(C))),attacker(C) -> attacker(B).
attacker(B),attacker(C) -> attacker(sencrypt(B,C)).
attacker(B),attacker(C) -> attacker(exp(B,C)).
mess(B,C),attacker(B) -> attacker(C).
attacker(c).
attacker(B),attacker(C) -> mess(B,C).
attacker(pk(skA)).
attacker(pk(skB)).
attacker(B) -> attacker(tuple_2(encrypt(tuple_2(pk(skA),'Ka'(B,C)),B),exp(tuple_base,x(B,C)))).
attacker(tuple_3(encrypt(B,pk(skA)),C,keyhash(tuple_4(exp(tuple_base,x(D,E)),C,D,pk(skA)),hash(tuple_2('Ka'(D,E),B))))),attacker(D) 
    -> attacker(keyhash(tuple_4(C,exp(tuple_base,x(D,E)),
	                          pk(skA),D),
                                  hash(tuple_2('Ka'(D,E),B)))).
attacker(tuple_3(encrypt(B,pk(skA)),C,keyhash(tuple_4(exp(tuple_base,x(pk(skB),D)),C,pk(skB),pk(skA)),hash(tuple_2('Ka'(pk(skB),D),B))))),attacker(pk(skB)) -> attacker(sencrypt(secretA,hash(exp(C,x(pk(skB),D))))).
attacker(tuple_2(encrypt(tuple_2(B,C),pk(skB)),D)) -> attacker(tuple_3(encrypt('Kb'(tuple_2(encrypt(tuple_2(B,C),pk(skB)),D),E),B),exp(tuple_base,y(tuple_2(encrypt(tuple_2(B,C),pk(skB)),D),E)),keyhash(tuple_4(D,exp(tuple_base,y(tuple_2(encrypt(tuple_2(B,C),pk(skB)),D),E)),pk(skB),B),hash(tuple_2(C,'Kb'(tuple_2(encrypt(tuple_2(B,C),pk(skB)),D),E)))))).
attacker(keyhash(tuple_4(exp(tuple_base,y(tuple_2(encrypt(tuple_2(pk(skA),B),pk(skB)),C),D)),C,pk(skA),pk(skB)),hash(tuple_2(B,'Kb'(tuple_2(encrypt(tuple_2(pk(skA),B),pk(skB)),C),D))))),attacker(tuple_2(encrypt(tuple_2(pk(skA),B),pk(skB)),C)) -> attacker(sencrypt(secretB,hash(exp(C,y(tuple_2(encrypt(tuple_2(pk(skA),B),pk(skB)),C),D))))).
attacker(secretB) -> [].
attacker(secretA) -> [].


top_predicates_precedence([mess,attacker]).
precedence([
keyhash,
pk,hash,sencrypt,encrypt,
'Ka','Kb',
exp,i,*,
tuple_4,tuple_3,tuple_2,tuple_base,
secretB,secretA,
1,
c,x,y,skA,skB]).