
Inductive val : Set :=
	v1 : val | v2 : val | v3 : val | v4 : val | v5 : val.

Definition agent (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => False
  | v3 => False
  | v4 => False
  | v5 => False
  end.

Definition alice : val := v1.

Definition alice_key_current (x1 x2 : val) : Prop :=
  match x1,x2 with
    v1,v1 => False
  | v1,v2 => True
  | v1,v3 => True
  | v1,v4 => True
  | v1,v5 => False
  | v2,v1 => True
  | v2,v2 => False
  | v2,v3 => True
  | v2,v4 => True
  | v2,v5 => True
  | v3,v1 => True
  | v3,v2 => True
  | v3,v3 => True
  | v3,v4 => True
  | v3,v5 => True
  | v4,v1 => True
  | v4,v2 => True
  | v4,v3 => True
  | v4,v4 => True
  | v4,v5 => True
  | v5,v1 => True
  | v5,v2 => True
  | v5,v3 => True
  | v5,v4 => True
  | v5,v5 => False
  end.

Definition alice_key_old(x1 x2:val) : Prop := True.

Definition bob : val := v1.

Definition bob_key_current(x1 x2:val) : Prop :=
  match x1,x2 with
    v1,v1 => False
  | v1,v2 => True
  | v1,v3 => True
  | v1,v4 => True
  | v1,v5 => False
  | v2,v1 => True
  | v2,v2 => True
  | v2,v3 => True
  | v2,v4 => True
  | v2,v5 => True
  | v3,v1 => True
  | v3,v2 => False
  | v3,v3 => True
  | v3,v4 => True
  | v3,v5 => True
  | v4,v1 => True
  | v4,v2 => True
  | v4,v3 => True
  | v4,v4 => True
  | v4,v5 => True
  | v5,v1 => False
  | v5,v2 => True
  | v5,v3 => True
  | v5,v4 => True
  | v5,v5 => False
  end.

Definition bob_key_old(x1 x2:val) : Prop := True.

Definition cons (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v5
  | v1,v2 => v3
  | v1,v3 => v4
  | v1,v4 => v4
  | v1,v5 => v5
  | v2,v1 => v4
  | v2,v2 => v3
  | v2,v3 => v3
  | v2,v4 => v4
  | v2,v5 => v3
  | v3,v1 => v4
  | v3,v2 => v3
  | v3,v3 => v2
  | v3,v4 => v2
  | v3,v5 => v2
  | v4,v1 => v4
  | v4,v2 => v4
  | v4,v3 => v3
  | v4,v4 => v4
  | v4,v5 => v2
  | v5,v1 => v5
  | v5,v2 => v4
  | v5,v3 => v2
  | v5,v4 => v4
  | v5,v5 => v5
  end.

Definition crypt (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v1
  | v1,v2 => v2
  | v1,v3 => v1
  | v1,v4 => v2
  | v1,v5 => v5
  | v2,v1 => v3
  | v2,v2 => v5
  | v2,v3 => v1
  | v2,v4 => v5
  | v2,v5 => v2
  | v3,v1 => v2
  | v3,v2 => v5
  | v3,v3 => v1
  | v3,v4 => v1
  | v3,v5 => v3
  | v4,v1 => v3
  | v4,v2 => v5
  | v4,v3 => v2
  | v4,v4 => v5
  | v4,v5 => v4
  | v5,v1 => v1
  | v5,v2 => v5
  | v5,v3 => v1
  | v5,v4 => v5
  | v5,v5 => v5
  end.

Definition i : val := v1.

Definition key (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v1
  | v1,v2 => v5
  | v1,v3 => v5
  | v1,v4 => v5
  | v1,v5 => v5
  | v2,v1 => v2
  | v2,v2 => v1
  | v2,v3 => v1
  | v2,v4 => v1
  | v2,v5 => v3
  | v3,v1 => v5
  | v3,v2 => v5
  | v3,v3 => v5
  | v3,v4 => v5
  | v3,v5 => v5
  | v4,v1 => v5
  | v4,v2 => v5
  | v4,v3 => v5
  | v4,v4 => v5
  | v4,v5 => v5
  | v5,v1 => v5
  | v5,v2 => v5
  | v5,v3 => v5
  | v5,v4 => v5
  | v5,v5 => v5
  end.

Definition knows_current (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => False
  | v3 => False
  | v4 => False
  | v5 => True
  end.

Definition knows_old (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v2 => False
  | v3 => False
  | v4 => False
  | v5 => True
  end.

Definition l (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v4
  | v1,v2 => v4
  | v1,v3 => v1
  | v1,v4 => v5
  | v1,v5 => v4
  | v2,v1 => v3
  | v2,v2 => v3
  | v2,v3 => v3
  | v2,v4 => v3
  | v2,v5 => v3
  | v3,v1 => v3
  | v3,v2 => v5
  | v3,v3 => v3
  | v3,v4 => v3
  | v3,v5 => v3
  | v4,v1 => v4
  | v4,v2 => v3
  | v4,v3 => v3
  | v4,v4 => v3
  | v4,v5 => v4
  | v5,v1 => v4
  | v5,v2 => v4
  | v5,v3 => v1
  | v5,v4 => v4
  | v5,v5 => v4
  end.

Definition nil : val := v1.
Definition prv : val := v3.
Definition pub : val := v1.

Definition s (x1 : val) : val :=
  match x1 with
    v1 => v5
  | v2 => v2
  | v3 => v3
  | v4 => v4
  | v5 => v5
  end.

Definition server : val := v1.

Definition session_current (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v1
  | v1,v2 => v5
  | v1,v3 => v5
  | v1,v4 => v5
  | v1,v5 => v1
  | v2,v1 => v5
  | v2,v2 => v5
  | v2,v3 => v5
  | v2,v4 => v5
  | v2,v5 => v5
  | v3,v1 => v5
  | v3,v2 => v5
  | v3,v3 => v5
  | v3,v4 => v5
  | v3,v5 => v5
  | v4,v1 => v5
  | v4,v2 => v5
  | v4,v3 => v5
  | v4,v4 => v5
  | v4,v5 => v5
  | v5,v1 => v1
  | v5,v2 => v1
  | v5,v3 => v5
  | v5,v4 => v1
  | v5,v5 => v1
  end.

Definition session_old (x1 x2 : val) : val :=
  match x1,x2 with
    v1,v1 => v2
  | v1,v2 => v2
  | v1,v3 => v2
  | v1,v4 => v2
  | v1,v5 => v2
  | v2,v1 => v4
  | v2,v2 => v2
  | v2,v3 => v2
  | v2,v4 => v2
  | v2,v5 => v2
  | v3,v1 => v2
  | v3,v2 => v4
  | v3,v3 => v4
  | v3,v4 => v4
  | v3,v5 => v2
  | v4,v1 => v4
  | v4,v2 => v2
  | v4,v3 => v4
  | v4,v4 => v2
  | v4,v5 => v4
  | v5,v1 => v4
  | v5,v2 => v2
  | v5,v3 => v2
  | v5,v4 => v2
  | v5,v5 => v4
  end.

Definition sym : val := v2.
Definition t_current : val := v5.
Definition t_old : val := v1.

Lemma lem_intruder_knows_session_key_as_seen_by_B : forall _big_kab:val, bob_key_current bob _big_kab -> knows_current _big_kab -> False.
Proof.
  intro _big_kab; case _big_kab; simpl; trivial.
Qed.

Lemma lem_intruder_knows_session_key_as_seen_by_alice : forall _big_kab:val, alice_key_current alice _big_kab -> knows_current _big_kab -> False.
Proof.
  intro _big_kab; case _big_kab; simpl; trivial.
Qed.

Lemma lem_intruder_knows_session_key_generated_by_server : knows_current (key sym (session_current alice bob)) -> False.
Proof.
  simpl; trivial.
Qed.

Lemma lem_define_bob_key_current : forall _big_a _big_b _big_kab X:val, knows_current (cons (crypt (cons t_current (cons (l X _big_b) (cons _big_kab (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) (cons (crypt (cons _big_a (cons t_current nil)) _big_kab) nil)) -> bob_key_current _big_b _big_kab.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro X; case X; simpl; trivial.
Qed.

Lemma lem_define_alice_key_current : forall _big_a _big_b _big_kab _big_msg:val, knows_current (crypt (s t_current) _big_kab) -> knows_current (crypt (cons t_current (cons (l _big_a _big_b) (cons _big_kab (cons _big_b (cons _big_msg nil))))) (key sym (cons _big_a (cons server nil)))) -> alice_key_current _big_a _big_kab.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro _big_msg; case _big_msg; simpl; trivial.
Qed.

Lemma lem_intruder_knows_timestamp_current : knows_current t_current.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_own_private_key_current : knows_current (key prv i).
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_every_public_key_current : forall X:val, knows_current (key pub X).
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_agents_current : forall X:val, agent X -> knows_current X.
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_current : forall _big_a _big_b _big_kab X:val, knows_current (cons (crypt (cons t_current (cons (l X _big_b) (cons _big_kab (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) (cons (crypt (cons _big_a (cons t_current nil)) _big_kab) nil)) -> knows_current (crypt (s t_current) _big_kab).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro X; case X; simpl; trivial.
Qed.

Lemma lem_alice_gets_server_message_and_forwards_submessage_to_bob_current : forall _big_a _big_b _big_kab _big_msg:val, knows_current (crypt (cons t_current (cons (l _big_a _big_b) (cons _big_kab (cons _big_b (cons _big_msg nil))))) (key sym (cons _big_a (cons server nil)))) -> knows_current (cons _big_msg (cons (crypt (cons _big_a (cons t_current nil)) _big_kab) nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro _big_msg; case _big_msg; simpl; trivial.
Qed.

Lemma lem_server_answers_A_with_encrypted_packet_current : forall _big_a _big_b:val, knows_current (cons _big_a (cons _big_b nil)) -> knows_current (crypt (cons t_current (cons (l _big_a _big_b) (cons (key sym (session_current _big_a _big_b)) (cons _big_b (cons (crypt (cons t_current (cons (l _big_a _big_b) (cons (key sym (session_current _big_a _big_b)) (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) nil))))) (key sym (cons _big_a (cons server nil)))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_alice_sends_message_1_to_server_current : forall _big_a _big_b:val, agent _big_b -> agent _big_a -> knows_current (cons _big_a (cons _big_b nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_current : forall _big_m:val, knows_current (s _big_m) -> knows_current _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_knows_timestamps_current : knows_current t_current.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_successors_current : forall _big_m:val, knows_current _big_m -> knows_current (s _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_symmetric_key_current : forall _big_m X:val, knows_current (crypt _big_m (key sym X)) -> knows_current (key sym X) -> knows_current _big_m.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_public_key_current : forall _big_k _big_m:val, knows_current (crypt _big_m (key prv _big_k)) -> knows_current (key pub _big_k) -> knows_current _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_private_key_current : forall _big_k _big_m:val, knows_current (crypt _big_m (key pub _big_k)) -> knows_current (key prv _big_k) -> knows_current _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_encrypt_current : forall _big_k _big_m:val, knows_current _big_m -> knows_current _big_k -> knows_current (crypt _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_build_pairs_current : forall _big_m1 _big_m2:val, knows_current _big_m1 -> knows_current _big_m2 -> knows_current (cons _big_m1 _big_m2).
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_second_components_current : forall _big_m1 _big_m2:val, knows_current (cons _big_m1 _big_m2) -> knows_current _big_m2.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_first_components_current : forall _big_m1 _big_m2:val, knows_current (cons _big_m1 _big_m2) -> knows_current _big_m1.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_knows_nil_current : knows_current nil.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_session_keys : forall _big_a _big_b:val, knows_current (key sym (session_old _big_a _big_b)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_remembers : forall _big_m:val, knows_old _big_m -> knows_current _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_define_bob_key_old : forall _big_a _big_b _big_kab X:val, knows_old (cons (crypt (cons t_old (cons (l X _big_b) (cons _big_kab (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) (cons (crypt (cons _big_a (cons t_old nil)) _big_kab) nil)) -> bob_key_old _big_b _big_kab.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro X; case X; simpl; try red; trivial.
Qed.

Lemma lem_define_alice_key_old : forall _big_a _big_b _big_kab _big_msg:val, knows_old (crypt (s t_old) _big_kab) -> knows_old (crypt (cons t_old (cons (l _big_a _big_b) (cons _big_kab (cons _big_b (cons _big_msg nil))))) (key sym (cons _big_a (cons server nil)))) -> alice_key_old _big_a _big_kab.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro _big_msg; case _big_msg; simpl; try red; trivial.
Qed.

Lemma lem_intruder_knows_timestamp_old : knows_old t_old.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_own_private_key_old : knows_old (key prv i).
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_knows_every_public_key_old : forall X:val, knows_old (key pub X).
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_agents_old : forall X:val, agent X -> knows_old X.
Proof.
  intro X; case X; simpl; trivial.
Qed.

Lemma lem_agent_B_gets_forwarded_submessage_and_sends_confirmation_challenge_old : forall _big_a _big_b _big_kab X:val, knows_old (cons (crypt (cons t_old (cons (l X _big_b) (cons _big_kab (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) (cons (crypt (cons _big_a (cons t_old nil)) _big_kab) nil)) -> knows_old (crypt (s t_old) _big_kab).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro X; case X; simpl; trivial.
Qed.

Lemma lem_alice_gets_server_message_and_forwards_submessage_to_bob_old : forall _big_a _big_b _big_kab _big_msg:val, knows_old (crypt (cons t_old (cons (l _big_a _big_b) (cons _big_kab (cons _big_b (cons _big_msg nil))))) (key sym (cons _big_a (cons server nil)))) -> knows_old (cons _big_msg (cons (crypt (cons _big_a (cons t_old nil)) _big_kab) nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_kab; case _big_kab; intro _big_msg; case _big_msg; simpl; trivial.
Qed.

Lemma lem_server_answers_A_with_encrypted_packet_old : forall _big_a _big_b:val, knows_old (cons _big_a (cons _big_b nil)) -> knows_old (crypt (cons t_old (cons (l _big_a _big_b) (cons (key sym (session_old _big_a _big_b)) (cons _big_b (cons (crypt (cons t_old (cons (l _big_a _big_b) (cons (key sym (session_old _big_a _big_b)) (cons _big_a nil)))) (key sym (cons _big_b (cons server nil)))) nil))))) (key sym (cons _big_a (cons server nil)))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_alice_sends_message_1_to_server_old : forall _big_a _big_b:val, agent _big_b -> agent _big_a -> knows_old (cons _big_a (cons _big_b nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_old : forall _big_m:val, knows_old (s _big_m) -> knows_old _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_knows_timestamps_old : knows_old t_old.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_successors_old : forall _big_m:val, knows_old _big_m -> knows_old (s _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_symmetric_key_old : forall _big_m X:val, knows_old (crypt _big_m (key sym X)) -> knows_old (key sym X) -> knows_old _big_m.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_public_key_old : forall _big_k _big_m:val, knows_old (crypt _big_m (key prv _big_k)) -> knows_old (key pub _big_k) -> knows_old _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_decrypt_if_has_private_key_old : forall _big_k _big_m:val, knows_old (crypt _big_m (key pub _big_k)) -> knows_old (key prv _big_k) -> knows_old _big_m.
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_encrypt_old : forall _big_k _big_m:val, knows_old _big_m -> knows_old _big_k -> knows_old (crypt _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_build_pairs_old : forall _big_m1 _big_m2:val, knows_old _big_m1 -> knows_old _big_m2 -> knows_old (cons _big_m1 _big_m2).
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_second_components_old : forall _big_m1 _big_m2:val, knows_old (cons _big_m1 _big_m2) -> knows_old _big_m2.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_can_take_first_components_old : forall _big_m1 _big_m2:val, knows_old (cons _big_m1 _big_m2) -> knows_old _big_m1.
Proof.
  intro _big_m1; case _big_m1; intro _big_m2; case _big_m2; simpl; trivial.
Qed.

Lemma lem_intruder_knows_nil_old : knows_old nil.
Proof.
  simpl; trivial.
Qed.

Lemma lem_intruder_agent : agent i.
Proof.
  simpl; trivial.
Qed.

Lemma lem_server_agent : agent server.
Proof.
  simpl; trivial.
Qed.

Lemma lem_bob_agent : agent bob.
Proof.
  simpl; trivial.
Qed.

Lemma lem_alice_agent : agent alice.
Proof.
  simpl; trivial.
Qed.
