%%% Challenge-Response %%%

%% Basic Actions %%
primitive_action(encrypt(_A,_M,_K)).
primitive_action(decrypt(_A,_M,_K)).
primitive_action(send(_A,_B,_M)).
primitive_action(receive(_A,_B,_M)).
primitive_action(makeNonce(_A)).
primitive_action(makePID(_A)).
primitive_action(compose(_A,_X1)).
primitive_action(compose(_A,_X1,_X2)).

%% Protocol Specific Actions %%
primitive_action(cr1s(_A,_B)).
primitive_action(cr1r2s(_A,_B,_M)).
primitive_action(cr2r(_A,_B,_M)).

%%% Successor State Axioms %%%

%% Relational Fluents %%
agent(G, do(_A,S)) :- agent(G,S).		restoreSitArg(agent(G),S,agent(G,S)).
intruder(G, do(_A,S)) :- intruder(G,S).		restoreSitArg(intruder(G),S,intruder(G,S)).
key(K, do(_A,S)) :- key(K,S).			restoreSitArg(key(K),S,key(K,S)).
symKey(K, do(_A,S)) :- symKey(K,S).		restoreSitArg(symKey(K),S,symKey(K,S)).
asymKey(K1,K2, do(_A,S)) :- asymKey(K1,K2,S).	restoreSitArg(asymKey(K1,K2),S,asymKey(K1,K2,S)).
pubKey(K, do(_A,S)) :- pubKey(K,S).		restoreSitArg(pubKey(K),S,pubKey(K,S)).
privKey(K, do(_A,S)) :- privKey(K,S).		restoreSitArg(privKey(K),S,privKey(K,S)).
shKey(GA,GB,K, do(_A,S)) :- shKey(GA,GB,K,S).	restoreSitArg(shKey(GA,GB,K),S,shKey(GA,GB,K,S)).

msg(M, do(A,S)) :- A = compose(_,_), next(NXT,S), M is NXT.
msg(M, do(A,S)) :- A = compose(_,_,_), next(NXT,S), M is NXT.
msg(M, do(A,S)) :- A = cr1s(_,_), next(NXT,S), M is NXT.
msg(M, do(A,S)) :- A = cr1s(_,_), next(NXT,S), M is NXT + 2.
msg(M, do(A,S)) :- A = cr1r2s(_,_,_), next(NXT,S), M is NXT.
msg(M, do(A,S)) :- msg(M, S).
restoreSitArg(msg(M),S,msg(M,S)).

encMsg(EM, do(A,S)) :- A = encrypt(_,M,K), EM = enc(M,K).
encMsg(EM, do(A,S)) :- A = cr1s(GA,GB), EM = enc(SM,K), next(NXT,S), SM is NXT + 2, shKey(GB,GA,K,S).
encMsg(EM, do(_,S)) :- encMsg(EM, S).
restoreSitArg(encMsg(EM),S,encMsg(EM,S)).

nonce(N, do(A,S)) :- A = makeNonce(_), next(NXT,S), N is NXT.
nonce(N, do(A,S)) :- A = cr1s(_,_), next(NXT,S), N is NXT + 3.
nonce(N, do(A,S)) :- nonce(N, S).
restoreSitArg(nonce(N),S,nonce(N,S)).

initiated(GA,P, do(A,S)) :- A = cr1s(GA,_), next(NXT,S), P is NXT + 1.
initiated(GA,P, do(A,S)) :- initiated(GA,P, S).
restoreSitArg(initiated(GA,P),S,initiated(GA,P,S)).

pid(P, do(A,S)) :- A = makePID(_), next(NXT,S), P is NXT.
pid(P, do(A,S)) :- A = cr1s(_,_), next(NXT,S), P is NXT + 1.
pid(P, do(A,S)) :- pid(P, S).
restoreSitArg(pid(P),S,pid(P,S)).

alive(GA, do(A,_)) :- A = cr1s(GA,_).
alive(GA, do(A,_)) :- A = cr1r2s(GA,_,_).
alive(GA, do(A,_)) :- A = cr2r(GA,_,_).
alive(GA, do(_,S)) :- alive(GA, S).
restoreSitArg(alive(GA),S,alive(GA,S)).

has(G,X, do(A,S)) :- A = makeNonce(G), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = makePID(G), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = encrypt(G,M,K), X = enc(M,K).
has(G,X, do(A,S)) :- A = decrypt(G,enc(M,_),_), X = M.
has(G,X, do(A,S)) :- A = decrypt(G,enc(M,_),_), first(M,X,S).
has(G,X, do(A,S)) :- A = decrypt(G,enc(M,_),_), second(M,X,S).
has(G,X, do(A,S)) :- A = receive(G,_,M), X = M.
has(G,X, do(A,S)) :- A = receive(G,_,M), first(M,X,S).
has(G,X, do(A,S)) :- A = receive(G,_,M), second(M,X,S).
has(G,X, do(A,S)) :- A = compose(G,_), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = compose(G,_,_), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = cr1s(G,GB), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = cr1s(G,GB), next(NXT,S), X is NXT + 1.
has(G,X, do(A,S)) :- A = cr1s(G,GB), next(NXT,S), X is NXT + 3.
has(G,X, do(A,S)) :- A = cr1s(G,GB), next(NXT,S), X is NXT + 2.
has(G,X, do(A,S)) :- A = cr1s(G,GB), next(NXT,S), SM is NXT + 2, X = enc(SM,K), shKey(G,GB,K,S).
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,M), X = M.
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,M), first(M,X,S).
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,M), second(M,X,S).
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,OM), second(OM,enc(TMP1,_),S), first(TMP1,X,S).
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,_), next(NXT,S), X is NXT.
has(G,X, do(A,S)) :- A = cr1r2s(G,GB,_), next(NXT,S), X is NXT + 1.
has(G,X, do(A,S)) :- A = cr2r(G,GB,M), X = M.
has(G,X, do(A,S)) :- A = cr2r(G,GB,M), first(M,X,S).
has(G,X, do(A,S)) :- A = cr2r(G,GB,M), second(M,X,S).
has(G,X, do(A,S)) :- has(G,X,S).
restoreSitArg(has(G,X),S,has(G,X,S)).

sent(GA,GB,M, do(A,S)) :- A = send(GA,GB,M).
sent(GA,GB,M, do(A,S)) :- A = cr1s(GA,GB), next(NXT,S), M is NXT.
sent(GA,GB,M, do(A,S)) :- A = cr1r2s(GA,GB,_), next(NXT,S), M is NXT.
sent(GA,GB,M, do(A,S)) :- sent(GA,GB,M,S), \+
		(
			A = receive(_,GA,M) ;
			A = cr1r2s(GB,GA,M) ;
			A = cr2r(GB,GA,M)
		).
restoreSitArg(sent(GA,GB,M),S,sent(GA,GB,M,S)).

recd(GA,GB,M, do(A,S)) :- A = receive(GA,GB,M).
recd(GA,GB,M, do(A,S)) :- A = cr1r2s(GA,GB,M).
recd(GA,GB,M, do(A,S)) :- A = cr2r(GA,GB,M).
recd(GA,GB,M, do(A,S)) :- recd(GA,GB,M, S).
restoreSitArg(recd(GA,GB,M),S,recd(GA,GB,M,S)).

completed(P, do(A,S)) :- A = cr2r(_,_,M), first(M,P,S).
completed(P, do(A,S)) :- completed(P, S).
restoreSitArg(completed(P),S,completed(P,S)).

expect(GA,GB,P,ST, do(A,S)) :- A = cr1s(GA,GB), ST = 2, next(NXT,S), P is NXT + 1.
expect(GA,GB,P,ST, do(A,S)) :- expect(GA,GB,P,ST,S), \+
		(
			A = cr2r(GA,GB,M), ST = 2, first(M,P,S)
		).
restoreSitArg(expect(GA,GB,P,ST),S,expect(GA,GB,P,ST,S)).


%% Functional Fluents %%

encKey(enc(M,K),K, do(A,S)) :- A = encrypt(_,M,K).
encKey(enc(M,K),K, do(A,S)) :- A = cr1s(GA,GB), next(NXT,S), M is NXT + 2, shKey(GA,GB,K,S).
encKey(enc(M,K),K, do(A,S)) :- encKey(enc(M,K),K, S).
restoreSitArg(encKey(enc(M,K),K),S,encKey(enc(M,K),K,S)).

type(P,X, do(A,S)) :- A = makePID(_), next(NXT,S), P is NXT, X = cr.
type(P,X, do(A,S)) :- A = cr1s(_,_), next(NXT,S), P is NXT + 1, X = cr.
type(P,X, do(A,S)) :- type(P,X, S).
restoreSitArg(type(P,X),S,type(P,X,S)).

first(M,X, do(A,S)) :- A = compose(_,X), next(NXT,S), M is NXT.
first(M,X, do(A,S)) :- A = compose(_,X,_), next(NXT,S), M is NXT.
first(M,X, do(A,S)) :- A = cr1s(_,_), next(NXT,S), M is NXT, X is NXT + 1.
first(M,X, do(A,S)) :- A = cr1s(_,_), next(NXT,S), M is NXT + 2, X is NXT + 3.
first(M,X, do(A,S)) :- A = cr1r2s(_,_,OM), next(NXT,S), M is NXT, first(OM,X,S).
first(M,X, do(A,S)) :- first(M,X, S).
restoreSitArg(first(M,X),S,first(M,X,S)).

second(M,X, do(A,S)) :- A = compose(_,_,X), next(NXT,S), M is NXT.
second(M,X, do(A,S)) :- A = cr1s(GA,GB), next(NXT,S), M is NXT + 0, X = enc(SM,K), SM is NXT + 2, shKey(GA,GB,K,S).
second(M,X, do(A,S)) :- A = cr1r2s(_,_,OM), next(NXT,S), M is NXT, second(OM,enc(TMP1,_),S), first(TMP1,X,S).
second(M,X, do(A,S)) :- second(M,X, S).
restoreSitArg(second(M,X),S,second(M,X,S)).

next(N, do(A,S)) :- A = makeNonce(_), next(NXT,S), N is NXT + 1.
next(N, do(A,S)) :- A = makePID(_), next(NXT,S), N is NXT + 1.
next(N, do(A,S)) :- A = compose(_,_), next(NXT,S), N is NXT + 1.
next(N, do(A,S)) :- A = compose(_,_,_), next(NXT,S), N is NXT + 1.
next(N, do(A,S)) :- A = cr1s(_,_), next(NXT,S), N is NXT + 4.
next(N, do(A,S)) :- A = cr1r2s(_,_,_), next(NXT,S), N is NXT + 1.
next(N, do(A,S)) :- next(N, S), \+
		(
			A = makeNonce(_) ;
			A = makePID(_) ;
			A = compose(_,_) ;
			A = compose(_,_,_) ;
			A = cr1s(_,_) ;
			A = cr1r2s(_,_)
		).
restoreSitArg(next(N),S,next(N,S)).

%% Preconditions %%

poss(makeNonce(A), S) :- intruder(A,S).
poss(makePID(A), S) :- intruder(A,S), \+ (pid(P,S), has(A,P,S), \+ initiated(_,P,S)).

poss(encrypt(A,M,K), S) :- intruder(A,S), msg(M,S), key(K,S), has(A,M,S), has(A,K,S), \+ has(A,enc(M,K),S).

poss(decrypt(A,M,K), S) :- intruder(A,S), encMsg(M,S), has(A,M,S), has(A,K,S), ((symKey(K,S), encKey(M,K,S)) ; (asymKey(K1,K,S), encKey(M,K1,S))), M = enc(IM,_), \+ has(A,IM,S).
poss(receive(A,B,M), S) :- intruder(A,S), agent(B,S), agent(C,S), msg(M,S), sent(B,C,M,S), \+ intruder(B,S), \+ has(A,M,S).

poss(send(A,B,M), S) :- agent(A,S), agent(B,S), msg(M,S), A \= B, \+ intruder(B,S), first(M,P,S), pid(P,S), has(intr,M,S), \+ sent(A,B,M,S). % Don't send something that's still waiting to be received

poss(compose(A,X1), S) :- intruder(A,S), has(A,X1,S), nonce(X1,S).
poss(compose(A,X1,X2), S) :- intruder(A,S), has(A,X1,S), has(A,X2,S), pid(X1,S), (encMsg(X2,S) ; nonce(X2,S)).

poss(cr1s(A,B), S) :- agent(A,S), agent(B,S), A \= B, has(A,K,S), shKey(A,B,K,S).
poss(cr1r2s(A,B,M), S) :- agent(A,S), agent(B,S), A \= B, msg(M,S), sent(B,A,M,S), first(M,P,S), type(P,cr,S), second(M,X,S), encKey(X,K,S), has(A,K,S).
poss(cr2r(A,B,M), S) :- agent(A,S), agent(B,S), A \= B, msg(M,S), sent(B,A,M,S), first(M,P,S), type(P,cr,S), expect(A,B,P,2,S).

%% Initial State %%
agent(bob,s0).
agent(alice,s0).
agent(intr,s0).
intruder(intr,s0).
key(k-bob,s0).
key(kp-bob,s0).
pubKey(k-bob,s0).
privKey(kp-bob,s0).
asymKey(k-bob, kp-bob,s0).
asymKey(kp-bob, k-bob,s0).
has(bob, k-bob,s0).
has(bob, kp-bob,s0).
shKey(bob, alice, k-alice/bob,s0).
has(bob, k-alice,s0).
key(k-bob/intr,s0).
symKey(k-bob/intr,s0).
shKey(bob, intr, k-bob/intr,s0).
has(bob, k-intr,s0).
key(k-alice,s0).
key(kp-alice,s0).
pubKey(k-alice,s0).
privKey(kp-alice,s0).
asymKey(k-alice, kp-alice,s0).
asymKey(kp-alice, k-alice,s0).
has(alice, k-alice,s0).
has(alice, kp-alice,s0).
key(k-alice/bob,s0).
symKey(k-alice/bob,s0).
shKey(alice, bob, k-alice/bob,s0).
has(alice, k-bob,s0).
key(k-alice/intr,s0).
symKey(k-alice/intr,s0).
shKey(alice, intr, k-alice/intr,s0).
has(alice, k-intr,s0).
key(k-intr,s0).
key(kp-intr,s0).
pubKey(k-intr,s0).
privKey(kp-intr,s0).
asymKey(k-intr, kp-intr,s0).
asymKey(kp-intr, k-intr,s0).
has(intr, k-intr,s0).
has(intr, kp-intr,s0).
shKey(intr, bob, k-bob/intr,s0).
has(intr, k-bob,s0).
shKey(intr, alice, k-alice/intr,s0).
has(intr, k-alice,s0).
has(alice,k-alice/bob,s0).
has(alice,k-alice/intr,s0).
has(bob,k-alice/bob,s0).
has(bob,k-bob/intr,s0).
has(intr,k-alice/intr,s0).
has(intr,k-bob/intr,s0).
has(bob,bob,s0).
has(bob,alice,s0).
has(bob,intr,s0).
has(alice,bob,s0).
has(alice,alice,s0).
has(alice,intr,s0).
has(intr,bob,s0).
has(intr,alice,s0).
has(intr,intr,s0).
next(1,s0).