theory simple6
begin

/* for each  generated fact A(x) by the rule GenA, the rule Rev will send it to the adversary which cand send it back. Moreover, since f is public, even if g is private, he can use f and take adventage of the equation in order to compute new messages  */
/* So both events of the form  Ba(x) and  Ca(x) can occur */
/* lemma  Ba_Rev ensures that the adversary can learn an 'x' generated by the rule GenA, only if it was "revealed" before using the rule Rev  */

functions: a/0[private], f/2
equations: f(x,x) = a


rule GenA:
[Fr(~y)]--[Aa(~y)]->[A(~y)]

rule Rev:
[A(x)]--[Rev(x)]->[Out(x)]

rule GenB:
[In(x)]--[Ba(x)]->[B(x)]

rule GenC:
[In(x), In(y)]--[Eq(x,f(y,y)), Ca(x)]->[C(x)]


rule GenC2:
[In(x)]--[Ca2(x)]->[C2(x)]

axiom Equality_Checks_Succeed: "All x y #i. Eq(x,y) @ i ==> x = y"

lemma exB:
  exists-trace
    "Ex x #i. Ba(x) @i
    "
lemma exC:
  exists-trace
    "Ex x #i. Ca(x) @i
    "

lemma exC2:
  exists-trace
    "Ex #i. Ca2(a) @i
    "
    
lemma Ba_Rev:
    "All x #i #k. (Ba(x) @i) & (Aa(x)@k)   ==> Ex #j. Rev(x)@j & j<i
    "
   
lemma Ca_Rev:
    "All x #i #k. (Ca(x) @i) & (Aa(x)@k)   ==> Ex #j. Rev(x)@j & j<i
    "
end