Inductive __aux_54 : term -> Prop :=
    intruder_knows_every_public_key_1 : (__aux_54 pub)
with agent : term -> Prop :=
    alice_is_an_agent : (agent alice)
  | bob_is_an_agent : (agent bob)
  | server_is_an_agent : (agent server)
  | intruder_is_an_agent : (agent intruder)
with __aux_57 : term -> Prop :=
    intruder_knows_own_private_key_2 : (__aux_57 intruder)
with __aux_59 : term -> Prop :=
    intruder_knows_all_previous_session_keys_2 : (_x1:term)(_x2:term)(_x3:term)(__aux_59 (old_session _x1 _x2 _x3))
with __aux_36 : term -> Prop :=
    intruder_knows_previous_server_messages_1 : (_x1:term)(_x2:term)(__aux_37 _x2) -> (__aux_18 _x1) -> (__aux_36 (cons _x1 _x2))
with __aux_28 : term -> Prop :=
    server_answers_A_with_encrypted_packet_11 : (_x1:term)(_x2:term)(__aux_30 _x2) -> (__aux_22 _x1) -> (__aux_28 (cons _x1 _x2))
with __aux_52 : term -> Prop :=
    alice_answers_confirmation_challenge_2 : (_x1:term)(_x2:term)(__aux_51 (__aux__vars11 _x2 _x1)) -> (__aux_52 (s _x1))
with reach_intruder_knows_session_key_generated_by_server : Prop :=
    intruder_knows_session_key_generated_by_server : (_x1:term)(knows (key sym (current_session alice bob _x1))) -> reach_intruder_knows_session_key_generated_by_server
with __aux_23 : term -> Prop :=
    server_answers_A_with_encrypted_packet_9 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_26 _x1) -> (__aux_23 (cons _x1 _x2))
with __aux_14 : term -> Prop :=
    alice_sends_message_1_to_server_8 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_9 _x1) -> (__aux_14 (cons _x1 _x2))
with reach_intruder_knows_session_key_as_seen_by_alice : Prop :=
    intruder_knows_session_key_as_seen_by_alice : (_x1:term)(alice_key _x1) -> (knows _x1) -> reach_intruder_knows_session_key_as_seen_by_alice
with __aux_56 : term -> Prop :=
    intruder_knows_own_private_key_1 : (__aux_56 prv)
with __aux_21 : term -> Prop :=
    server_answers_A_with_encrypted_packet_5 : (_x1:term)(_x2:term)(__aux_23 _x2) -> (__aux_22 _x1) -> (__aux_21 (cons _x1 _x2))
with __aux_55 : term -> Prop :=
    intruder_knows_every_public_key_2 : (_x1:term)(__aux_55 _x1)
with __aux_22 : term -> Prop :=
    server_answers_A_with_encrypted_packet_12 : (_x1:term)(_x2:term)(__aux_25 _x2) -> (__aux_24 _x1) -> (__aux_22 (key _x1 _x2))
  | server_answers_A_with_encrypted_packet_6 : (_x1:term)(_x2:term)(__aux_25 _x2) -> (__aux_24 _x1) -> (__aux_22 (key _x1 _x2))
with __aux_7 : term -> Prop :=
    alice_sends_message_1_to_server_7 : (__aux_7 alice)
  | alice_sends_message_1_to_server_1 : (__aux_7 alice)
with __aux_9 : term -> Prop :=
    alice_sends_message_1_to_server_3 : (__aux_9 bob)
  | alice_sends_message_1_to_server_9 : (__aux_9 bob)
with knows : term -> Prop :=
    intruder_knows_nil : (knows nil)
  | intruder_can_take_first_components : (_x1:term)(_x2:term)(knows (cons _x1 _x2)) -> (knows _x1)
  | intruder_can_take_second_components : (_x1:term)(_x2:term)(knows (cons _x2 _x1)) -> (knows _x1)
  | intruder_can_build_pairs : (_x1:term)(_x2:term)(knows _x2) -> (knows _x1) -> (knows (cons _x1 _x2))
  | intruder_can_encrypt : (_x1:term)(_x2:term)(knows _x2) -> (knows _x1) -> (knows (crypt _x1 _x2))
  | intruder_can_decrypt_if_has_private_key : (_x1:term)(_x2:term)(__aux_2 (__aux__vars2 _x1 _x2)) -> (__aux_1 (__aux__vars1 _x2)) -> (knows _x1)
  | intruder_can_decrypt_if_has_public_key : (_x1:term)(_x2:term)(__aux_4 (__aux__vars4 _x1 _x2)) -> (__aux_3 (__aux__vars3 _x2)) -> (knows _x1)
  | intruder_can_decrypt_if_has_symmetric_key : (_x1:term)(_x2:term)(__aux_6 (__aux__vars6 _x1 _x2)) -> (__aux_5 (__aux__vars5 _x2)) -> (knows _x1)
  | intruder_can_compute_successors : (_x1:term)(knows _x1) -> (knows (s _x1))
  | intruder_can_compute_predecessors : (_x1:term)(knows (s _x1)) -> (knows _x1)
  | alice_sends_message_1_to_server : (_x1:term)(_x2:term)(__aux_8 _x2) -> (__aux_7 _x1) -> (knows (cons _x1 _x2))
  | server_answers_A_with_encrypted_packet : (_x1:term)(_x2:term)(__aux_17 _x2) -> (__aux_16 _x1) -> (knows (crypt _x1 _x2))
  | intruder_knows_previous_server_messages : (_x1:term)(_x2:term)(__aux_17 _x2) -> (__aux_36 _x1) -> (knows (crypt _x1 _x2))
  | alice_gets_server_message_and_forwards_submessage_to_bob : (_x1:term)(_x2:term)(__aux_44 (__aux__vars8 _x1 _x2)) -> (knows _x1)
  | agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge : (_x1:term)(_x2:term)(__aux_50 _x2) -> (__aux_49 _x1) -> (knows (crypt _x1 _x2))
  | intruder_knows_all_agents : (_x1:term)(agent _x1) -> (knows _x1)
  | alice_answers_confirmation_challenge_1 : (_x1:term)(_x2:term)(__aux_53 _x2) -> (__aux_52 _x1) -> (knows (crypt _x1 _x2))
  | intruder_knows_every_public_key : (_x1:term)(_x2:term)(__aux_55 _x2) -> (__aux_54 _x1) -> (knows (key _x1 _x2))
  | intruder_knows_own_private_key : (_x1:term)(_x2:term)(__aux_57 _x2) -> (__aux_56 _x1) -> (knows (key _x1 _x2))
  | intruder_knows_all_previous_session_keys : (_x1:term)(_x2:term)(__aux_59 _x2) -> (__aux_58 _x1) -> (knows (key _x1 _x2))
with __aux_19 : term -> Prop :=
    server_answers_A_with_encrypted_packet_3 : (_x1:term)(_x2:term)(__aux_21 _x2) -> (__aux_20 _x1) -> (__aux_19 (cons _x1 _x2))
with __aux_25 : term -> Prop :=
    server_answers_A_with_encrypted_packet_8 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_25 (current_session _x1 _x2 _x3))
  | server_answers_A_with_encrypted_packet_14 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_25 (current_session _x1 _x2 _x3))
with __aux_26 : term -> Prop :=
    server_answers_A_with_encrypted_packet_10 : (_x1:term)(_x2:term)(__aux_29 _x2) -> (__aux_28 _x1) -> (__aux_26 (crypt _x1 _x2))
with __aux_53 : term -> Prop :=
    alice_answers_confirmation_challenge_3 : (_x1:term)(_x2:term)(__aux_51 (__aux__vars11 _x1 _x2)) -> (__aux_53 _x1)
with reach_intruder_knows_session_key_as_seen_by_B : Prop :=
    intruder_knows_session_key_as_seen_by_B : (_x1:term)(_x2:term)(_x3:term)(knows (crypt (s (nonceb _x1 _x2 _x3)) _x1)) -> (knows _x1) -> reach_intruder_knows_session_key_as_seen_by_B
with __aux_13 : term -> Prop :=
    alice_sends_message_1_to_server_6 : (_x1:term)(_x2:term)(__aux_14 _x2) -> (__aux_7 _x1) -> (__aux_13 (cons _x1 _x2))
with __aux_51 : term -> Prop :=
    alice_answers_confirmation_challenge_4 : (_x1:term)(_x2:term)(knows (crypt _x2 _x1)) -> (alice_key _x1) -> (__aux_51 (__aux__vars11 _x1 _x2))
with __aux_12 : term -> Prop :=
    alice_sends_message_1_to_server_11 : (__aux_12 nil)
  | alice_sends_message_1_to_server_10 : (__aux_12 nil)
with __aux_11 : term -> Prop :=
    alice_sends_message_1_to_server_5 : (_x1:term)(__aux_13 _x1) -> (__aux_11 (noncea _x1))
with __aux_58 : term -> Prop :=
    intruder_knows_all_previous_session_keys_1 : (__aux_58 sym)
with __aux_10 : term -> Prop :=
    alice_sends_message_1_to_server_4 : (_x1:term)(_x2:term)(__aux_12 _x2) -> (__aux_11 _x1) -> (__aux_10 (cons _x1 _x2))
with __aux_16 : term -> Prop :=
    server_answers_A_with_encrypted_packet_1 : (_x1:term)(_x2:term)(__aux_19 _x2) -> (__aux_18 _x1) -> (__aux_16 (cons _x1 _x2))
with __aux_49 : term -> Prop :=
    agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_1 : (_x1:term)(_x2:term)(_x3:term)(__aux_48 (__aux__vars10 _x2 _x3 _x1)) -> (__aux_49 (nonceb _x1 _x2 _x3))
with __aux_27 : term -> Prop :=
    server_answers_A_with_encrypted_packet_32 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | server_answers_A_with_encrypted_packet_24 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | server_answers_A_with_encrypted_packet_25 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | server_answers_A_with_encrypted_packet_17 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | intruder_knows_previous_server_messages_32 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | intruder_knows_previous_server_messages_25 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | intruder_knows_previous_server_messages_24 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
  | intruder_knows_previous_server_messages_17 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_27 nil)
with __aux_42 : term -> Prop :=
    intruder_knows_previous_server_messages_10 : (_x1:term)(_x2:term)(__aux_29 _x2) -> (__aux_43 _x1) -> (__aux_42 (crypt _x1 _x2))
with __aux_48 : term -> Prop :=
    agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_3 : (_x1:term)(_x2:term)(_x3:term)(knows (crypt (cons _x3 (cons _x1 nil)) (key sym (cons _x2 (cons server nil))))) -> (__aux_48 (__aux__vars10 _x1 _x2 _x3))
with __aux_41 : term -> Prop :=
    intruder_knows_previous_server_messages_8 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_41 (old_session _x1 _x2 _x3))
  | intruder_knows_previous_server_messages_14 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_41 (old_session _x1 _x2 _x3))
with alice_key : term -> Prop :=
    alice_gets_server_message_and_stores_current_session_key : (_x1:term)(_x2:term)(__aux_47 _x2) -> (__aux_46 _x1) -> (alice_key (key _x1 _x2))
with __aux_32 : term -> Prop :=
    server_answers_A_with_encrypted_packet_20 : (_x1:term)(_x2:term)(__aux_33 _x2) -> (__aux_20 _x1) -> (__aux_32 (cons _x1 _x2))
  | intruder_knows_previous_server_messages_20 : (_x1:term)(_x2:term)(__aux_33 _x2) -> (__aux_20 _x1) -> (__aux_32 (cons _x1 _x2))
with __aux_38 : term -> Prop :=
    intruder_knows_previous_server_messages_5 : (_x1:term)(_x2:term)(__aux_40 _x2) -> (__aux_39 _x1) -> (__aux_38 (cons _x1 _x2))
with __aux_30 : term -> Prop :=
    server_answers_A_with_encrypted_packet_15 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_31 _x1) -> (__aux_30 (cons _x1 _x2))
  | intruder_knows_previous_server_messages_15 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_31 _x1) -> (__aux_30 (cons _x1 _x2))
with __aux_44 : term -> Prop :=
    alice_gets_server_message_and_forwards_submessage_to_bob_1 : (_x1:term)(_x2:term)(knows (crypt (cons (noncea (cons alice (cons bob nil))) (cons bob (cons _x2 (cons _x1 nil)))) (key sym (cons alice (cons server nil))))) -> (__aux_44 (__aux__vars8 _x1 _x2))
with __aux_43 : term -> Prop :=
    intruder_knows_previous_server_messages_11 : (_x1:term)(_x2:term)(__aux_30 _x2) -> (__aux_39 _x1) -> (__aux_43 (cons _x1 _x2))
with __aux_29 : term -> Prop :=
    server_answers_A_with_encrypted_packet_18 : (_x1:term)(_x2:term)(__aux_32 _x2) -> (__aux_24 _x1) -> (__aux_29 (key _x1 _x2))
  | intruder_knows_previous_server_messages_18 : (_x1:term)(_x2:term)(__aux_32 _x2) -> (__aux_24 _x1) -> (__aux_29 (key _x1 _x2))
with __aux_17 : term -> Prop :=
    server_answers_A_with_encrypted_packet_26 : (_x1:term)(_x2:term)(__aux_35 _x2) -> (__aux_24 _x1) -> (__aux_17 (key _x1 _x2))
  | intruder_knows_previous_server_messages_26 : (_x1:term)(_x2:term)(__aux_35 _x2) -> (__aux_24 _x1) -> (__aux_17 (key _x1 _x2))
with __aux_8 : term -> Prop :=
    alice_sends_message_1_to_server_2 : (_x1:term)(_x2:term)(__aux_10 _x2) -> (__aux_9 _x1) -> (__aux_8 (cons _x1 _x2))
with __aux_4 : term -> Prop :=
    intruder_can_decrypt_if_has_public_key_1 : (_x1:term)(_x2:term)(knows (crypt _x1 (key prv _x2))) -> (__aux_4 (__aux__vars4 _x1 _x2))
with __aux_46 : term -> Prop :=
    alice_gets_server_message_and_stores_current_session_key_1 : (_x1:term)(_x2:term)(_x3:term)(_x4:term)(_x5:term)(__aux_45 (__aux__vars9 _x2 _x3 _x4 _x5 _x1)) -> (__aux_46 _x1)
with __aux_37 : term -> Prop :=
    intruder_knows_previous_server_messages_3 : (_x1:term)(_x2:term)(__aux_38 _x2) -> (__aux_20 _x1) -> (__aux_37 (cons _x1 _x2))
with __aux_33 : term -> Prop :=
    server_answers_A_with_encrypted_packet_22 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_34 _x1) -> (__aux_33 (cons _x1 _x2))
  | server_answers_A_with_encrypted_packet_30 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_34 _x1) -> (__aux_33 (cons _x1 _x2))
  | intruder_knows_previous_server_messages_30 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_34 _x1) -> (__aux_33 (cons _x1 _x2))
  | intruder_knows_previous_server_messages_22 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_34 _x1) -> (__aux_33 (cons _x1 _x2))
with __aux_35 : term -> Prop :=
    server_answers_A_with_encrypted_packet_28 : (_x1:term)(_x2:term)(__aux_33 _x2) -> (__aux_31 _x1) -> (__aux_35 (cons _x1 _x2))
  | intruder_knows_previous_server_messages_28 : (_x1:term)(_x2:term)(__aux_33 _x2) -> (__aux_31 _x1) -> (__aux_35 (cons _x1 _x2))
with __aux_31 : term -> Prop :=
    server_answers_A_with_encrypted_packet_29 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_31 _x1)
  | server_answers_A_with_encrypted_packet_16 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_31 _x1)
  | intruder_knows_previous_server_messages_29 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_31 _x1)
  | intruder_knows_previous_server_messages_16 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_31 _x1)
with __aux_24 : term -> Prop :=
    server_answers_A_with_encrypted_packet_7 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | server_answers_A_with_encrypted_packet_27 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | server_answers_A_with_encrypted_packet_19 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | server_answers_A_with_encrypted_packet_13 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | intruder_knows_previous_server_messages_19 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | intruder_knows_previous_server_messages_13 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | intruder_knows_previous_server_messages_27 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
  | intruder_knows_previous_server_messages_7 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_24 sym)
with __aux_50 : term -> Prop :=
    agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_2 : (_x1:term)(_x2:term)(_x3:term)(__aux_48 (__aux__vars10 _x2 _x3 _x1)) -> (__aux_50 _x1)
with __aux_20 : term -> Prop :=
    server_answers_A_with_encrypted_packet_21 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x1 _x3)) -> (__aux_20 _x1)
  | server_answers_A_with_encrypted_packet_4 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x1 _x3)) -> (__aux_20 _x1)
  | intruder_knows_previous_server_messages_4 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x1 _x3)) -> (__aux_20 _x1)
  | intruder_knows_previous_server_messages_21 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x1 _x3)) -> (__aux_20 _x1)
with __aux_18 : term -> Prop :=
    server_answers_A_with_encrypted_packet_2 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x3 _x1)) -> (__aux_18 _x1)
  | intruder_knows_previous_server_messages_2 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x2 _x3 _x1)) -> (__aux_18 _x1)
with __aux_15 : term -> Prop :=
    server_answers_A_with_encrypted_packet_33 : (_x1:term)(_x2:term)(_x3:term)(knows (cons _x1 (cons _x2 (cons _x3 nil)))) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3))
  | intruder_knows_previous_server_messages_33 : (_x1:term)(_x2:term)(_x3:term)(knows (cons _x1 (cons _x2 (cons _x3 nil)))) -> (__aux_15 (__aux__vars7 _x1 _x2 _x3))
with __aux_40 : term -> Prop :=
    intruder_knows_previous_server_messages_9 : (_x1:term)(_x2:term)(__aux_27 _x2) -> (__aux_42 _x1) -> (__aux_40 (cons _x1 _x2))
with __aux_2 : term -> Prop :=
    intruder_can_decrypt_if_has_private_key_1 : (_x1:term)(_x2:term)(knows (crypt _x1 (key pub _x2))) -> (__aux_2 (__aux__vars2 _x1 _x2))
with __aux_45 : term -> Prop :=
    alice_gets_server_message_and_stores_current_session_key_3 : (_x1:term)(_x2:term)(_x3:term)(_x4:term)(_x5:term)(knows (crypt (cons (noncea (cons alice (cons bob nil))) (cons bob (cons (key _x5 (current_session _x3 _x1 _x2)) (cons _x4 nil)))) (key sym (cons alice (cons server nil))))) -> (__aux_45 (__aux__vars9 _x1 _x2 _x3 _x4 _x5))
with __aux_5 : term -> Prop :=
    intruder_can_decrypt_if_has_symmetric_key_2 : (_x1:term)(knows (key sym _x1)) -> (__aux_5 (__aux__vars5 _x1))
with __aux_1 : term -> Prop :=
    intruder_can_decrypt_if_has_private_key_2 : (_x1:term)(knows (key prv _x1)) -> (__aux_1 (__aux__vars1 _x1))
with __aux_3 : term -> Prop :=
    intruder_can_decrypt_if_has_public_key_2 : (_x1:term)(knows (key pub _x1)) -> (__aux_3 (__aux__vars3 _x1))
with __aux_34 : term -> Prop :=
    server_answers_A_with_encrypted_packet_23 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_34 server)
  | server_answers_A_with_encrypted_packet_31 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_34 server)
  | intruder_knows_previous_server_messages_23 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_34 server)
  | intruder_knows_previous_server_messages_31 : (_x1:term)(_x2:term)(_x3:term)(__aux_15 (__aux__vars7 _x1 _x2 _x3)) -> (__aux_34 server)
with __aux_6 : term -> Prop :=
    intruder_can_decrypt_if_has_symmetric_key_1 : (_x1:term)(_x2:term)(knows (crypt _x1 (key sym _x2))) -> (__aux_6 (__aux__vars6 _x1 _x2))
with __aux_39 : term -> Prop :=
    intruder_knows_previous_server_messages_12 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (__aux_39 (key _x1 _x2))
  | intruder_knows_previous_server_messages_6 : (_x1:term)(_x2:term)(__aux_41 _x2) -> (__aux_24 _x1) -> (__aux_39 (key _x1 _x2))
with __aux_47 : term -> Prop :=
    alice_gets_server_message_and_stores_current_session_key_2 : (_x1:term)(_x2:term)(_x3:term)(_x4:term)(_x5:term)(__aux_45 (__aux__vars9 _x2 _x3 _x1 _x4 _x5)) -> (__aux_47 (current_session _x1 _x2 _x3))
.
