input_clause(intruder_knows_nil, axiom,
          [
          ++knows( nil )
          ]).

input_clause(intruder_can_take_first_components, axiom,
          [
          --knows( cons( M1 , M2 ) ),
          ++knows( M1 )
          ]).

input_clause(intruder_can_take_second_components, axiom,
          [
          --knows( cons( M1 , M2 ) ),
          ++knows( M2 )
          ]).

input_clause(intruder_can_build_pairs, axiom,
          [
          --knows( M1 ) ,
          --knows( M2 ),
          ++knows( cons( M1 , M2 ) )
          ]).

input_clause(intruder_can_encrypt, axiom,
          [
          --knows( M ) ,
          --knows( K ),
          ++knows( crypt( M , K ) )
          ]).

input_clause(intruder_can_decrypt_if_has_private_key, axiom,
          [
          --knows( crypt( M , key (pub, K) ) ) ,
          --knows( key (prv, K) ),
          ++knows( M )
          ]).

input_clause(intruder_can_decrypt_if_has_public_key, axiom,
          [
          --knows( crypt( M , key (prv, K) ) ) ,
          --knows( key (pub, K) ),
          ++knows( M )
          ]).

input_clause(intruder_can_decrypt_if_has_symmetric_key, axiom,
          [
          --knows( crypt( M , key (sym, X) ) ) ,
          --knows( key (sym, X)),
          ++knows( M )
          ]).

input_clause(intruder_can_compute_successors, axiom,
	  [
          --knows (M),
	  ++knows (s (M))
          ]).

input_clause (intruder_can_compute_predecessors, axiom,
	  [
          --knows (s (M)),
	  ++knows (M)
          ]).

input_clause(alice_sends_message_1_to_server, axiom,
          [
	  ++knows (cons (alice,
	           cons (bob,
		   cons (noncea (alice, bob),
		         nil))))
          ]).

input_clause(server_answers_A_with_encrypted_packet, axiom,
          [
	  --knows (cons (A, cons (B, cons (Na, nil)))),
	  ++knows (crypt (cons (Na,
                          cons (B,
                          cons (key (sym, current_session (A, B, Na)),
			  cons (crypt (cons (key (sym, current_session (A, B, Na)),
			               cons (A,
				             nil)),
				     key (sym, cons (B, cons (server, nil)))),
				nil)))),
		        key (sym, cons (A, cons (server, nil)))))
          ]).

input_clause(intruder_knows_previous_server_messages, axiom,
          [
	  --knows (cons (A, cons (B, cons (Na, nil)))),
	  ++knows (crypt (cons (Na,
                          cons (B,
                          cons (key (sym, old_session (A, B, Na)),
			  cons (crypt (cons (key (sym, old_session (A, B, Na)),
			               cons (A,
				             nil)),
				     key (sym, cons (B, cons (server, nil)))),
				nil)))),
		        key (sym, cons (A, cons (server, nil)))))
          ]).

input_clause(alice_gets_server_message_and_forwards_submessage_to_bob, axiom,
          [
	  --knows (crypt (cons (noncea (alice, bob),
	                  cons (bob,
			  cons (Kab,
			  cons (Msg,
			        nil)))),
			key (sym, cons (alice, cons (server, nil))))),
	  ++knows (Msg)
          ]).

input_clause(alice_gets_server_message_and_stores_current_session_key, axiom,
          [
	  --knows (crypt (cons (noncea (alice, bob),
	                  cons (bob,
			  cons (Kab,
			  cons (Msg,
			        nil)))),
			key (sym, cons (alice, cons (server, nil))))),
	  ++alice_key (Kab)
          ]).

input_clause(agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge, axiom,
	  [
          --knows (crypt (cons (Kab,
	                  cons (A,
			        nil)),
			key (sym, cons (B, cons (server, nil))))),
	  ++knows (crypt (nonceb (Kab, A, B),
	                Kab))
          ]).

input_clause(alice_answers_confirmation_challenge, axiom,
	  [
          --alice_key (Kab),
          --knows (crypt (Nb, Kab)),
	  ++knows (crypt (s (Nb), Kab))
          ]).

input_clause(agent_B_checks_confirmation_from_A, axiom,
	[
	--knows (crypt (s (nonceb (Kab, A, B)), Kab)),
	++bob_key (Kab)
	]).

input_clause(alice_is_an_agent, axiom,
	  [
          ++agent(alice)
          ]).


input_clause(bob_is_an_agent, axiom,
	  [
          ++agent(bob)
          ]).


input_clause(server_is_an_agent, axiom,
	  [
          ++agent(server)
          ]).


input_clause(intruder_is_an_agent, axiom,
	  [
          ++agent(intruder)
          ]).

input_clause(intruder_knows_all_agents, axiom,
	  [
          --agent(X),
	  ++knows(X)
          ]).

input_clause(intruder_knows_every_public_key, axiom,
          [
          ++knows( key (pub, X) )
          ]).

input_clause(intruder_knows_own_private_key, axiom,
          [
          ++knows( key (prv, intruder) )
          ]).

input_clause(intruder_knows_all_previous_session_keys, axiom,
	[
        ++knows (key (sym, old_session (A, B, Na)))
        ]).

input_clause(intruder_knows_session_key_generated_by_server, conjecture, 
	[
        --knows (key (sym, current_session (alice, bob, Na)))
        ]).

input_clause(intruder_knows_session_key_as_seen_by_alice, conjecture,
	[
        --alice_key (key (Mode, current_session (X, Y, N))),
        --knows (key (Mode, current_session (X, Y, N)))
        ]).

input_clause(intruder_knows_session_key_as_seen_by_B, conjecture,
	[
        --knows (crypt (s (nonceb (Kab, A, B)),
                     Kab)),
        --knows (Kab)
        ]).