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

Definition agent (x1 : val) : Prop :=
  match x1 with
  | v1 => True
  | _ => 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 => False
  | v1,v4 => True
  | v2,v1 => True
  | v2,v2 => True
  | v2,v3 => True
  | v2,v4 => True
  | v3,v1 => True
  | v3,v2 => True
  | v3,v3 => True
  | v3,v4 => True
  | v4,v1 => True
  | v4,v2 => True
  | v4,v3 => True
  | v4,v4 => True
  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 => False
  | v1,v4 => False
  | v2,v1 => False
  | v2,v2 => True
  | v2,v3 => True
  | v2,v4 => False
  | v3,v1 => False
  | v3,v2 => True
  | v3,v3 => True
  | v3,v4 => False
  | v4,v1 => False
  | v4,v2 => True
  | v4,v3 => True
  | v4,v4 => False
  end.

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

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

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

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

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

Definition i : val := v1.

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

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

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

Definition nil : val := v1.

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

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

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

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

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

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

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

Definition prv : val := v3.

Definition pub : val := v1.

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

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

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

Definition server : val := v1.

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

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

Definition sym : val := v2.

Definition testable_current (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v4 => True
  | _ => False
  end.

Definition testable_old (x1 : val) : Prop :=
  match x1 with
    v1 => True
  | v4 => True
  | _ => False
  end.

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

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

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

Lemma lem_testable_dec_key_dec_current : forall _big_m X:val, knows_current (enc _big_m X) -> testable_current _big_m -> testable_current X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_dec_key_current : forall _big_m X:val, knows_current _big_m -> testable_current (dec _big_m X) -> testable_current X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_enc_key_dec_current : forall _big_m X:val, knows_current (dec _big_m X) -> testable_current _big_m -> testable_current X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_enc_key_current : forall _big_m X:val, knows_current _big_m -> testable_current (enc _big_m X) -> testable_current X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

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

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

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

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

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

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

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

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

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

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

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

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

Lemma lem_testable_succ_pred_current : forall _big_m:val, testable_current _big_m -> testable_current (p _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_testable_pred_pred_current : forall _big_m:val, testable_current (p _big_m) -> testable_current _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_second_testable_current : forall _big_l _big_m:val, testable_current _big_l -> testable_current (cons _big_m _big_l).
Proof.
  intro _big_l; case _big_l; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_first_testable_current : forall _big_l _big_m:val, testable_current _big_m -> testable_current (cons _big_m _big_l).
Proof.
  intro _big_l; case _big_l; intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_intruder_weak_secret_dec_dec_current : forall _big_m _big_p:val, testable_current _big_m -> testable_current (dec _big_m _big_p) -> knows_current _big_p.
Proof.
  intro _big_m; case _big_m; intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_weak_secret_dec_current : forall _big_m _big_p:val, testable_current (enc _big_m _big_p) -> testable_current _big_m -> knows_current _big_p.
Proof.
  intro _big_m; case _big_m; intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_knows_agents_public_key_current : forall X:val, agent X -> 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_define_bob_key_dec_current : forall _big_a _big_b _big_m _big_na:val, knows_current (crypt (nonceb_current _big_a _big_b) (key sym (r_current _big_a _big_b))) -> knows_current (crypt _big_na (key sym (r_current _big_a _big_b))) -> knows_current (cons _big_a (cons _big_m nil)) -> bob_key_current _big_a (r_current _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_define_bob_key_current : forall _big_a _big_b _big_ka _big_na:val, knows_current (crypt (nonceb_current _big_a _big_b) (key sym (r_current _big_a _big_b))) -> knows_current (crypt _big_na (key sym (r_current _big_a _big_b))) -> knows_current (cons _big_a (cons (enc _big_ka (passwd_current _big_a _big_b)) nil)) -> bob_key_current _big_a (r_current _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_define_alice_key_current : forall _big_a _big_b _big_nb _big_r:val, knows_current (crypt (cons (noncea_current _big_a _big_b) (cons _big_nb nil)) (key sym _big_r)) -> knows_current (enc (crypt _big_r (key pub (session_current _big_a _big_b))) (passwd_current _big_a _big_b)) -> alice_key_current _big_a _big_r.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_nb; case _big_nb; intro _big_r; case _big_r; simpl; trivial.
Qed.

Lemma lem_message5_current : forall _big_a _big_b _big_nb _big_r:val, knows_current (crypt (cons (noncea_current _big_a _big_b) (cons _big_nb nil)) (key sym _big_r)) -> knows_current (enc (crypt _big_r (key pub (session_current _big_a _big_b))) (passwd_current _big_a _big_b)) -> knows_current (crypt _big_nb (key sym _big_r)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_nb; case _big_nb; intro _big_r; case _big_r; simpl; trivial.
Qed.

Lemma lem_message4_dec_current : forall _big_a _big_b _big_m _big_na:val, knows_current (crypt _big_na (key sym (r_current _big_a _big_b))) -> knows_current (cons _big_a (cons _big_m nil)) -> knows_current (crypt (cons _big_na (cons (nonceb_current _big_a _big_b) nil)) (key sym (r_current _big_a _big_b))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_message4_current : forall _big_a _big_b _big_ka _big_na:val, knows_current (crypt _big_na (key sym (r_current _big_a _big_b))) -> knows_current (cons _big_a (cons (enc _big_ka (passwd_current _big_a _big_b)) nil)) -> knows_current (crypt (cons _big_na (cons (nonceb_current _big_a _big_b) nil)) (key sym (r_current _big_a _big_b))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_message3_current : forall _big_a _big_b _big_r:val, knows_current (enc (crypt _big_r (key pub (session_current _big_a _big_b))) (passwd_current _big_a _big_b)) -> knows_current (crypt (noncea_current _big_a _big_b) (key sym _big_r)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_r; case _big_r; simpl; trivial.
Qed.

Lemma lem_message2_dec_current : forall _big_a _big_b _big_m:val, knows_current (cons _big_a (cons _big_m nil)) -> knows_current (enc (crypt (r_current _big_a _big_b) (dec _big_m (passwd_current _big_a _big_b))) (passwd_current _big_a _big_b)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_message2_current : forall _big_a _big_b _big_ka:val, knows_current (cons _big_a (cons (enc _big_ka (passwd_current _big_a _big_b)) nil)) -> knows_current (enc (crypt (r_current _big_a _big_b) _big_ka) (passwd_current _big_a _big_b)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; simpl; trivial.
Qed.

Lemma lem_message1_current : forall _big_a _big_b:val, agent _big_b -> agent _big_a -> knows_current (cons _big_a (cons (enc (key pub (session_current _big_a _big_b)) (passwd_current _big_a _big_b)) nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_can_dec_enc_current : forall _big_k _big_m:val, knows_current _big_k -> knows_current (enc _big_m _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_dec_current : forall _big_k _big_m:val, knows_current _big_k -> knows_current _big_m -> knows_current (dec _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_enc_dec_current : forall _big_k _big_m:val, knows_current _big_k -> knows_current (dec _big_m _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_enc_current : forall _big_k _big_m:val, knows_current _big_k -> knows_current _big_m -> knows_current (enc _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_succ_current : forall _big_m:val, knows_current _big_m -> knows_current (p _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_compute_successors_pred_current : forall _big_m:val, knows_current (p _big_m) -> knows_current _big_m.
Proof.
  intro _big_m; case _big_m; 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_nonceb : forall _big_a _big_b:val, knows_current (nonceb_old _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_noncea : forall _big_a _big_b:val, knows_current (noncea_old _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_knows_all_previous_passwords : forall _big_a _big_b:val, knows_current (passwd_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_intruder_knows_own_private_key_old : knows_old (key prv i).
Proof.
  simpl; trivial.
Qed.

Lemma lem_testable_dec_key_dec_old : forall _big_m X:val, knows_old (enc _big_m X) -> testable_old _big_m -> testable_old X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_dec_key_old : forall _big_m X:val, knows_old _big_m -> testable_old (dec _big_m X) -> testable_old X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_enc_key_dec_old : forall _big_m X:val, knows_old (dec _big_m X) -> testable_old _big_m -> testable_old X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

Lemma lem_testable_enc_key_old : forall _big_m X:val, knows_old _big_m -> testable_old (enc _big_m X) -> testable_old X.
Proof.
  intro _big_m; case _big_m; intro X; case X; simpl; trivial.
Qed.

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

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

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

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

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

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

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

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

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

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

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

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


Lemma lem_testable_succ_pred_old : forall _big_m:val, testable_old _big_m -> testable_old (p _big_m).
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_testable_pred_pred_old : forall _big_m:val, testable_old (p _big_m) -> testable_old _big_m.
Proof.
  intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_second_testable_old : forall _big_l _big_m:val, testable_old _big_l -> testable_old (cons _big_m _big_l).
Proof.
  intro _big_l; case _big_l; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_first_testable_old : forall _big_l _big_m:val, testable_old _big_m -> testable_old (cons _big_m _big_l).
Proof.
  intro _big_l; case _big_l; intro _big_m; case _big_m; simpl; trivial.
Qed.

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

Lemma lem_intruder_weak_secret_dec_dec_old : forall _big_m _big_p:val, testable_old _big_m -> testable_old (dec _big_m _big_p) -> knows_old _big_p.
Proof.
  intro _big_m; case _big_m; intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_weak_secret_dec_old : forall _big_m _big_p:val, testable_old (enc _big_m _big_p) -> testable_old _big_m -> knows_old _big_p.
Proof.
  intro _big_m; case _big_m; intro _big_p; case _big_p; simpl; trivial.
Qed.

Lemma lem_intruder_knows_agents_public_key_old : forall X:val, agent X -> 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_define_bob_key_dec_old : forall _big_a _big_b _big_m _big_na:val, knows_old (crypt (nonceb_old _big_a _big_b) (key sym (r_old _big_a _big_b))) -> knows_old (crypt _big_na (key sym (r_old _big_a _big_b))) -> knows_old (cons _big_a (cons _big_m nil)) -> bob_key_old _big_a (r_old _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; intro _big_na; case _big_na;
  simpl; try red; trivial.
Qed.

Lemma lem_define_bob_key_old : forall _big_a _big_b _big_ka _big_na:val, knows_old (crypt (nonceb_old _big_a _big_b) (key sym (r_old _big_a _big_b))) -> knows_old (crypt _big_na (key sym (r_old _big_a _big_b))) -> knows_old (cons _big_a (cons (enc _big_ka (passwd_old _big_a _big_b)) nil)) -> bob_key_old _big_a (r_old _big_a _big_b).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; intro _big_na; case _big_na;
  simpl; try red; trivial.
Qed.

Lemma lem_define_alice_key_old : forall _big_a _big_b _big_nb _big_r:val, knows_old (crypt (cons (noncea_old _big_a _big_b) (cons _big_nb nil)) (key sym _big_r)) -> knows_old (enc (crypt _big_r (key pub (session_old _big_a _big_b))) (passwd_old _big_a _big_b)) -> alice_key_old _big_a _big_r.
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_nb; case _big_nb; intro _big_r; case _big_r;
  simpl; try red; trivial.
Qed.

Lemma lem_message5_old : forall _big_a _big_b _big_nb _big_r:val, knows_old (crypt (cons (noncea_old _big_a _big_b) (cons _big_nb nil)) (key sym _big_r)) -> knows_old (enc (crypt _big_r (key pub (session_old _big_a _big_b))) (passwd_old _big_a _big_b)) -> knows_old (crypt _big_nb (key sym _big_r)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_nb; case _big_nb; intro _big_r; case _big_r; simpl; trivial.
Qed.

Lemma lem_message4_dec_old : forall _big_a _big_b _big_m _big_na:val, knows_old (crypt _big_na (key sym (r_old _big_a _big_b))) -> knows_old (cons _big_a (cons _big_m nil)) -> knows_old (crypt (cons _big_na (cons (nonceb_old _big_a _big_b) nil)) (key sym (r_old _big_a _big_b))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_message4_old : forall _big_a _big_b _big_ka _big_na:val, knows_old (crypt _big_na (key sym (r_old _big_a _big_b))) -> knows_old (cons _big_a (cons (enc _big_ka (passwd_old _big_a _big_b)) nil)) -> knows_old (crypt (cons _big_na (cons (nonceb_old _big_a _big_b) nil)) (key sym (r_old _big_a _big_b))).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; intro _big_na; case _big_na; simpl; trivial.
Qed.

Lemma lem_message3_old : forall _big_a _big_b _big_r:val, knows_old (enc (crypt _big_r (key pub (session_old _big_a _big_b))) (passwd_old _big_a _big_b)) -> knows_old (crypt (noncea_old _big_a _big_b) (key sym _big_r)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_r; case _big_r; simpl; trivial.
Qed.

Lemma lem_message2_dec_old : forall _big_a _big_b _big_m:val, knows_old (cons _big_a (cons _big_m nil)) -> knows_old (enc (crypt (r_old _big_a _big_b) (dec _big_m (passwd_old _big_a _big_b))) (passwd_old _big_a _big_b)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_message2_old : forall _big_a _big_b _big_ka:val, knows_old (cons _big_a (cons (enc _big_ka (passwd_old _big_a _big_b)) nil)) -> knows_old (enc (crypt (r_old _big_a _big_b) _big_ka) (passwd_old _big_a _big_b)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b;
  intro _big_ka; case _big_ka; simpl; trivial.
Qed.

Lemma lem_message1_old : forall _big_a _big_b:val, agent _big_b -> agent _big_a -> knows_old (cons _big_a (cons (enc (key pub (session_old _big_a _big_b)) (passwd_old _big_a _big_b)) nil)).
Proof.
  intro _big_a; case _big_a; intro _big_b; case _big_b; simpl; trivial.
Qed.

Lemma lem_intruder_can_dec_enc_old : forall _big_k _big_m:val, knows_old _big_k -> knows_old (enc _big_m _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_dec_old : forall _big_k _big_m:val, knows_old _big_k -> knows_old _big_m -> knows_old (dec _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_enc_dec_old : forall _big_k _big_m:val, knows_old _big_k -> knows_old (dec _big_m _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_enc_old : forall _big_k _big_m:val, knows_old _big_k -> knows_old _big_m -> knows_old (enc _big_m _big_k).
Proof.
  intro _big_k; case _big_k; intro _big_m; case _big_m; simpl; trivial.
Qed.

Lemma lem_intruder_can_compute_predecessors_succ_old : forall _big_m:val, knows_old _big_m -> knows_old (p _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_compute_successors_pred_old : forall _big_m:val, knows_old (p _big_m) -> knows_old _big_m.
Proof.
  intro _big_m; case _big_m; 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.

