begin_problem(Unknown).

list_of_descriptions.
name({*Neumann-Stubblebine*}).
author({*Georg Moser*}).
status(satisfiable).
description({* formula set G 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))))).
end_of_list.

list_of_formulae(conjectures).
  formula(exists([x],and(Ak(key(x,b)),Bk(key(x,a))))).
end_of_list.

end_problem.