begin_problem(fmc09_homework2).
list_of_descriptions.
name({*FMC 2009, homework 2, solution*}).
author({*Dominique Unruh*}).
status(unsatisfiable).
description({* *}).
end_of_list.

list_of_symbols.
  % We define function symbols for all constructors, and for the
  % protocol nonces that appear in the protocol. We use a generic
  % function advnonce to model adversary-nonces. That is,
  % adversary-nonces are of the form advnonce(whatever).
  functions[(enc,2),(hash,1),(advnonce,1),(Nsecret,0),(K1,0),(K2,0)].

  % We model two predicates for the adversary knowledge.
  % knows1(x) means that S1|-x
  % knows2(x) means that S2|-x
  predicates[ (knows1,1), (knows2,1) ].
end_of_list.

list_of_formulae(axioms).
  % Deduction rules for S1|-...
  formula(forall([x],knows1(advnonce(x)))).
  formula(forall([x,y],implies(and(knows1(x),knows1(y)),knows1(enc(x,y))))).
  formula(forall([x],knows1(hash(x)))).
  formula(forall([x,y],implies(and(knows1(enc(x,y)),knows1(x)),knows1(y)))).
  
  % Deduction rules for S2|-...
  % These are the same as for S1|-... 
  formula(forall([x],knows2(advnonce(x)))).
  formula(forall([x,y],implies(and(knows2(x),knows2(y)),knows2(enc(x,y))))).
  formula(forall([x],knows2(hash(x)))).
  formula(forall([x,y],implies(and(knows2(enc(x,y)),knows2(x)),knows2(y)))).

  % Definition of the set S1
  % Instead of defining S1, we give axioms S1|-x for all x\in S1
  formula(knows1(hash(K1))).
  formula(knows1(enc(K1,K2))).

  % Definition of the set S2
  % Instead of defining S2, we give axioms S2|-x for all x\in S2
  formula(knows2(hash(K1))).
  formula(knows2(enc(K1,K2))).
  % It is difficult in SPASS to say "let K' be a term such that
  % knows1(enc(K1,K'))". Instead, we just say "for all K' with
  % knows1(enc(K1,K')), let enc(K',Nsecret)\in S2".
  % (This constitutes an overapproximation.)
  formula(forall([k],implies(knows1(enc(K1,k)),knows2(enc(k,Nsecret))))).


  % Assuming a bad hash function, we need to add the rules 
  % S_i|-hash(x) ==> S_i|-x for i=1,2.
  % Thus, for the second part of the problem, uncomment the following
  % two lines:
  
  %formula(forall([x],implies(knows1(hash(x)),knows1(x)))).
  %formula(forall([x],implies(knows2(hash(x)),knows2(x)))).
end_of_list.

list_of_formulae(conjectures).
  formula(knows2(Nsecret)).
end_of_list.

end_problem.