begin_problem(Unknown).

list_of_descriptions.
name({*Neumann-Stubblebine*}).
author({*Georg Moser*}).
status(satisfiable).
description({* formula set H in lecture notes *}).
end_of_list.

list_of_symbols.
  functions[(pair,2),(triple,3),(quadr,4),(key,2),(sent,3),(encr,2),(kt,1),(a,0),(b,0),
	(t,0),(bt,0),(at,0),(na,0),(nb,1),(tb,1)].
  predicates[(M,1),(Ak,1),(Sa,1),(Bk,1),(Sb,1),(Tk,1),(Bf,1),(P,1),(Im,1),(Ik,1),(Nonce,1)].
end_of_list.

list_of_formulae(axioms).

%PRINCIPAL A
  formula(Ak(key(at,t))).
  formula(P(a)).
  formula(and(M(sent(a,b,pair(a,na))),Sa(pair(b,na)))).
  formula(forall([xnb,xbet,xk,xm,xb,xna],
	implies(and(M(sent(t,a,triple(encr(quadr(xb,xna,xk,xbet),at),xm,xnb))),
		    Sa(pair(xb,xna))),
		and(M(sent(a,xb,pair(xm,encr(xnb,xk)))),
		    Ak(key(xk,xb)))))).
%PRINCIPAL B
  formula(Bk(key(bt,t))).
  formula(P(b)).
  formula(Bf(na)).	
  formula(forall([xa,xna],
	implies(and(M(sent(xa,b,pair(xa,xna))),Bf(xna)),
	        and(M(sent(b,t,triple(b,nb(xna),encr(triple(xa,xna,tb(xna)),bt)))),
		    Sb(pair(xa,xna)))))).
  formula(forall([xbet,xk,xnb,xa,xna],
	implies(and(M(sent(xa,b,pair(encr(triple(xa,xk,tb(xna)),bt),encr(nb(xna),xk)))),
		    Sb(pair(xa,xna))),
	   Bk(key(xk,xa))))).


%PRINCIPAL T
  formula(and(Tk(key(at,a)),Tk(key(bt,b)))).
  formula(P(t)).
  formula(forall([xb,xnb,xa,xna,xbet,xbt,xat,xk],
	implies(and(M(sent(xb,t,triple(xb,xnb,encr(triple(xa,xna,xbet),xbt)))),
			Tk(key(xbt,xb)),Tk(key(xat,xa)),Nonce(xna)),
	M(sent(t,xa,triple(encr(quadr(xb,xna,kt(xna),xbet),xat),
			  encr(triple(xa,kt(xna),xbet),xbt),
			  xnb)))))).
  formula(Nonce(na)).
  formula(forall([x],not(Nonce(kt(x))))).
  formula(forall([x],and(Nonce(tb(x)),Nonce(nb(x))))).

%INTRUDER I
  formula(forall([xa,xb,xm],implies(M(sent(xa,xb,xm)),Im(xm)))).
  formula(forall([u,v],implies(Im(pair(u,v)),and(Im(u),Im(v))))).
  formula(forall([u,v,w],implies(Im(triple(u,v,w)),and(Im(u),Im(v),Im(w))))).
  formula(forall([u,v,w,z],implies(Im(quadr(u,v,w,z)),and(Im(u),Im(v),Im(w),Im(z))))).
  formula(forall([u,v,w],implies(and(Im(encr(u,v)),Ik(key(v,w)),P(w)),Im(v)))).	

  formula(forall([u,v],implies(and(Im(u),Im(v)), Im(pair(u,v))))).
  formula(forall([u,v,w],implies(and(Im(u),Im(v),Im(w)), Im(triple(u,v,w))))).
  formula(forall([u,v,w,x],implies(and(Im(u),Im(v),Im(w),Im(x)), Im(quadr(u,v,w,x))))).
  formula(forall([u,x,y],implies(and(Im(u),P(x),P(y)), M(sent(x,y,u))))).

  formula(forall([u,v,w],implies(and(Im(v),P(w)),Ik(key(v,w))))).
  formula(forall([u,v,w],implies(and(Im(u),Ik(key(v,w)),P(w)),Im(encr(u,v))))).	

end_of_list.

list_of_formulae(conjectures).

  formula(exists([x],and(Ik(key(x,b)),Bk(key(x,a))))).

end_of_list.

end_problem.