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

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

Definition alice : val := v3.

Definition bob : val := v3.

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

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

Definition f1 (x1 x2 x3 : val) : val :=
  match x1,x2,x3 with
  | v1,v1,v1 => v2
  | v1,v1,v2 => v1
  | v1,v1,v3 => v3
  | v1,v2,v1 => v1
  | v1,v2,v2 => v3
  | v1,v2,v3 => v2
  | v1,v3,v1 => v2
  | v1,v3,v2 => v2
  | v1,v3,v3 => v3
  | v2,v1,v1 => v2
  | v2,v1,v2 => v1
  | v2,v1,v3 => v3
  | v2,v2,v1 => v1
  | v2,v2,v2 => v3
  | v2,v2,v3 => v2
  | v2,v3,v1 => v2
  | v2,v3,v2 => v2
  | v2,v3,v3 => v1
  | v3,v1,v1 => v1
  | v3,v1,v2 => v1
  | v3,v1,v3 => v2
  | v3,v2,v1 => v3
  | v3,v2,v2 => v1
  | v3,v2,v3 => v2
  | v3,v3,v1 => v2
  | v3,v3,v2 => v2
  | v3,v3,v3 => v1
  end.

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

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

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

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

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

Definition i : val := v3.

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

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

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

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

Definition nil : val := v1.

Definition nonces_current (x1 x2 x3 : val) : val := 
  match x1,x2,x3 with
  | v1,v1,v1 => v2
  | v1,v1,v2 => v3
  | v1,v1,v3 => v3
  | v1,v2,v1 => v2
  | v1,v2,v2 => v3
  | v1,v2,v3 => v2
  | v1,v3,v1 => v2
  | v1,v3,v2 => v2
  | v1,v3,v3 => v3
  | v2,v1,v1 => v2
  | v2,v1,v2 => v2
  | v2,v1,v3 => v1
  | v2,v2,v1 => v1
  | v2,v2,v2 => v2
  | v2,v2,v3 => v1
  | v2,v3,v1 => v2
  | v2,v3,v2 => v3
  | v2,v3,v3 => v1
  | v3,v1,v1 => v3
  | v3,v1,v2 => v3
  | v3,v1,v3 => v3
  | v3,v2,v1 => v2
  | v3,v2,v2 => v3
  | v3,v2,v3 => v3
  | v3,v3,v1 => v2
  | v3,v3,v2 => v2
  | v3,v3,v3 => v3
  end.

Definition nonces_old (x1 x2 x3 : val) : val := 
  match x1,x2,x3 with
  | v1,v1,v1 => v2
  | v1,v1,v2 => v1
  | v1,v1,v3 => v1
  | v1,v2,v1 => v1
  | v1,v2,v2 => v3
  | v1,v2,v3 => v1
  | v1,v3,v1 => v3
  | v1,v3,v2 => v1
  | v1,v3,v3 => v1
  | v2,v1,v1 => v3
  | v2,v1,v2 => v3
  | v2,v1,v3 => v2
  | v2,v2,v1 => v3
  | v2,v2,v2 => v1
  | v2,v2,v3 => v1
  | v2,v3,v1 => v3
  | v2,v3,v2 => v3
  | v2,v3,v3 => v3
  | v3,v1,v1 => v3
  | v3,v1,v2 => v1
  | v3,v1,v3 => v1
  | v3,v2,v1 => v3
  | v3,v2,v2 => v3
  | v3,v2,v3 => v1
  | v3,v3,v1 => v1
  | v3,v3,v2 => v1
  | v3,v3,v3 => v2
  end.

Definition peer_keys_current (x1 x2 x3 : val) : Prop := True.

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

Definition prv : val := v2.
Definition pub : val := v1.
Definition request_id : val := v1.
Definition respond_id : val := v1.

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

Definition server : val := v3.

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

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

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

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

Definition success : val := v1.
Definition sym : val := v1.


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

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

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

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

Lemma lem_intruder_knows_nil_old : knows_old nil.
Proof.
  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_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_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_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_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_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_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_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_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_can_hash_old : forall _big_m:val, knows_old _big_m -> knows_old (h _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_message1_old : knows_old request_id.
Proof.
  simpl; trivial.
Qed.

Lemma lem_message2_old : forall _big_p:val, agent _big_p -> knows_old request_id -> knows_old (cons respond_id (nai _big_p)).
Proof.
  intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_message3_old : forall _big_nAI _big_p _big_s:val, agent _big_s -> agent _big_p -> knows_old (cons respond_id (cons _big_nAI nil)) -> knows_old (cons (nonces_old _big_nAI _big_s _big_p) (cons (cons (crypt (session_old _big_nAI _big_s _big_p) (f5 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p))) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) (session_old _big_nAI _big_s _big_p) (nonces_old _big_nAI _big_s _big_p)) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) nil)))) (cons (nonces_old _big_nAI _big_s _big_p) (cons (cons (crypt (session_old _big_nAI _big_s _big_p) (f5 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p))) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) (session_old _big_nAI _big_s _big_p) (nonces_old _big_nAI _big_s _big_p)) nil)) nil)))) nil))).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_message4_old : forall _big_nAI _big_ns _big_p _big_s _big_sqn:val, knows_old (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) nil)))) nil))) -> knows_old request_id -> knows_old (cons (f2 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil))) nil)).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_ns; case _big_ns;
  intro _big_p; case _big_p; intro _big_s; case _big_s;
  intro _big_sqn; case _big_sqn; simpl; trivial.
Qed.

Lemma lem_message5_old : forall _big_nAI _big_p _big_s:val, knows_old (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) nil))) nil)) -> knows_old (cons respond_id (cons _big_nAI nil)) -> knows_old success.
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_define_server_keys_old : forall _big_nAI _big_p _big_s:val, knows_old (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) nil))) nil)) -> knows_old (cons respond_id (cons _big_nAI nil)) -> server_keys_old _big_s (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)) (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_old _big_nAI _big_s _big_p)).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_define_peer_keys_old : forall _big_nAI _big_ns _big_p _big_s _big_sqn:val, knows_old success -> knows_old (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) nil)))) nil))) -> knows_old request_id -> peer_keys_old _big_p (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_ns; case _big_ns;
  intro _big_p; case _big_p; intro _big_s; case _big_s;
  intro _big_sqn; case _big_sqn; 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_intruder_knows_previous_server_IK : forall _big_cK _big_iK _big_s:val, server_keys_old _big_s _big_iK _big_cK -> knows_current _big_iK.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_intruder_knows_previous_server_CK : forall _big_cK _big_iK _big_s:val, server_keys_old _big_s _big_iK _big_cK -> knows_current _big_cK.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_intruder_knows_previous_peer_IK : forall _big_cK _big_iK _big_p:val, peer_keys_old _big_p _big_iK _big_cK -> knows_current _big_iK.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_knows_previous_peer_CK : forall _big_cK _big_iK _big_p:val, peer_keys_old _big_p _big_iK _big_cK -> knows_current _big_cK.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_knows_nil_current : knows_current nil.
Proof.
  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_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_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_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_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_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_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_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_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_can_hash_current : forall _big_m:val, knows_current _big_m -> knows_current (h _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_message1_current : knows_current request_id.
Proof.
  simpl; trivial.
Qed.

Lemma lem_message2_current : forall _big_p:val, agent _big_p -> knows_current request_id -> knows_current (cons respond_id (nai _big_p)).
Proof.
  intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_message3_current : forall _big_nAI _big_p _big_s:val, agent _big_s -> agent _big_p -> knows_current (cons respond_id (cons _big_nAI nil)) -> knows_current (cons (nonces_current _big_nAI _big_s _big_p) (cons (cons (crypt (session_current _big_nAI _big_s _big_p) (f5 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p))) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) (session_current _big_nAI _big_s _big_p) (nonces_current _big_nAI _big_s _big_p)) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) nil)))) (cons (nonces_current _big_nAI _big_s _big_p) (cons (cons (crypt (session_current _big_nAI _big_s _big_p) (f5 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p))) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) (session_current _big_nAI _big_s _big_p) (nonces_current _big_nAI _big_s _big_p)) nil)) nil)))) nil))).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_message4_current : forall _big_nAI _big_ns _big_p _big_s _big_sqn:val, knows_current (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) nil)))) nil))) -> knows_current request_id -> knows_current (cons (f2 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil))) nil)).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_ns; case _big_ns;
  intro _big_p; case _big_p; intro _big_s; case _big_s;
  intro _big_sqn; case _big_sqn; simpl; trivial.
Qed.

Lemma lem_message5_current : forall _big_nAI _big_p _big_s:val, knows_current (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) nil))) nil)) -> knows_current (cons respond_id (cons _big_nAI nil)) -> knows_current success.
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_define_server_keys_current : forall _big_nAI _big_p _big_s:val, knows_current (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) nil)))) (cons (f2 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) nil))) nil)) -> knows_current (cons respond_id (cons _big_nAI nil)) -> server_keys_current _big_s (f4 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)) (f3 (key sym (cons _big_s (cons _big_p nil))) (nonces_current _big_nAI _big_s _big_p)).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_p; case _big_p;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_define_peer_keys_current : forall _big_nAI _big_ns _big_p _big_s _big_sqn:val, knows_current success -> knows_current (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) (cons (h (cons (h (cons _big_nAI (cons (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (cons (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns) nil)))) (cons _big_ns (cons (cons (crypt _big_sqn (f5 (key sym (cons _big_s (cons _big_p nil))) _big_ns)) (cons (f1 (key sym (cons _big_s (cons _big_p nil))) _big_sqn _big_ns) nil)) nil)))) nil))) -> knows_current request_id -> peer_keys_current _big_p (f4 (key sym (cons _big_s (cons _big_p nil))) _big_ns) (f3 (key sym (cons _big_s (cons _big_p nil))) _big_ns).
Proof.
  intro _big_nAI; case _big_nAI; intro _big_ns; case _big_ns;
  intro _big_p; case _big_p; intro _big_s; case _big_s;
  intro _big_sqn; case _big_sqn; simpl; trivial.
Qed.

Lemma lem_intruder_knows_server_IK : forall _big_cK _big_iK _big_s:val, knows_current _big_iK -> server_keys_current _big_s _big_iK _big_cK -> False.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_s; case _big_s; simpl; trivial.
Qed.

Lemma lem_intruder_knows_server_CK : forall _big_cK _big_iK _big_s:val, knows_current _big_cK -> server_keys_current _big_s _big_iK _big_cK -> False.
Proof.
  intro _big_cK; case _big_cK; intro _big_iK; case _big_iK;
  intro _big_s; case _big_s; simpl; trivial.
Qed.
