How do I prove this property in Coq?

Question

I am working on a variant of an example by Christine Paulin-Mohring. It represents in Coq the Needham-Schroeder protocol in the (flawed) public key version. I would like to prove that the protocol is defective, but I frankly do not know where to start. It seems that the few tactics that I know are insufficient. Can someone suggest a way to approach the proof? Thank you for bearing me and my beginner question.

Inductive agent : Set := A | B | I. (* Alice, Bob, Intruder *)

Inductive message : Set := 
  Name : agent -> message  (* agent names *)
| Nonce : agent -> message (* a nonce is tagged with the agent who made it *)
| Enc : agent -> message -> message (* an agent encrypts a message with his/her public key *)
| C : message -> message -> message. (* concat of two messages *)

(* send X m = agent X sends message m 
 * receive X m = agent X receives message m
 * Note that agents CANNOT read the X parameter, 
 * they can read only the message m. Also, they
 * CANNOT read the Y parameter of the (Nonce Y)
 * nonces they receive.
 *)
Inductive send : agent -> message -> Prop :=
  (* Alice and Bob can only send the three handshake messages *)
  msg1 : forall X Y, (X = A \/ X = B)             (* no assumption on Y *)
         -> send X (Enc Y (C (Name X) (Nonce X)))
| msg2 : forall X Y Z, (X = A \/ X = B)           (* no assumption on Y Z *)
         -> receive X (Enc X (C (Name Y) (Nonce Z)))
         -> send X (Enc Y (C (Name X) (C (Nonce X) (Nonce Z))))
| msg3 : forall X Y Z, (X = A \/ X = B)           (* no assumption on Y Z *)
         -> receive X (Enc X (C (Name Y) (C (Nonce Z) (Nonce X))))
         -> send X (Enc Y (Nonce Z))
(* Intruder can send whatever (s)he knows *)
| intruder : forall m, known m -> send I m
(* everyone receives everything *)
with receive : agent -> message -> Prop :=
  bcast : forall X Y m, send X m -> receive Y m
(* what the intruder knows (messages): this includes
 * all agent names (background knowledge), the content 
 * of the messages (s)he can observe, decrypt and forge *)
with known : message -> Prop :=
  spy : forall m, receive I m -> known m
| name : forall a, known (Name a)
| decomp_l : forall m m', known (C m m') -> known m
| decomp_r : forall m m', known (C m m') -> known m'
| compose : forall m m', known m -> known m' -> known (C m m')
| crypt : forall X m , known m -> known (Enc X m)
| decrypt : forall m, known (Enc I m) -> known m
(* definition of a bad handshake between X and Y *)
with bad_hs : agent -> agent -> Prop :=
  _bhs : forall X Y, (X = A \/ X = B) -> (Y = A \/ Y = B) -> X <> Y
       -> receive I (Enc I (C (Name X) (Nonce X)))               (* msg1 *)
       -> receive Y (Enc Y (C (Name I) (Nonce X)))               (* msg1 spoofed *)
       -> receive X (Enc X (C (Name I) (C (Nonce Y) (Nonce X)))) (* msg2 *)
       -> receive Y (Enc Y (Nonce Y))                            (* msg3 *)
       -> bad_hs X Y.

(* the flaw in the protocol: a bad handshake allows
 * the intruder to know the secrets and play the
 * man-in-the-middle.
 *)
Theorem flaw : exists X Y, bad_hs X Y /\ known (Nonce X) /\ known (Nonce Y).
(* sketch of a proof:
 * 1: send A (Enc I (C (Name A) (Nonce A)))                   | msg1(A, I)
 * 2: receive I (Enc I (C (Name A) (Nonce A)))                | bcast(1, I)
 * 3: known (Enc I (C (Name A) (Nonce A)))                    | spy(2)
 * 4: known (C (Name A) (Nonce A))                            | decrypt(3)
 * 5: known (Nonce A)                                         | decomp_r(4)
 * 6: known (Name I)                                          | name(I)
 * 7: known (C (Name I) (Nonce A))                            | compose(6, 5)
 * 8: known (Enc B (C (Name I) (Nonce A)))                    | crypt(B, 7)
 * 9: send I (Enc B (C (Name I) (Nonce A)))                   | intruder(8)
 * 10: receive B (Enc B (C (Name I) (Nonce A)))               | bcast(9, B)
 * 11: send B (Enc I (C (Name B) (C (Nonce B) (Nonce A))))    | msg2(10)
 * 12: receive I (Enc I (C (Name B) (C (Nonce B) (Nonce A)))) | bcast(11, I)
 * 13: known (Enc I (C (Name B) (C (Nonce B) (Nonce A))))     | spy(12)
 * 14: known (C (Name B) (C (Nonce B) (Nonce A)))             | decrypt(13)
 * 15: known (C (Nonce B) (Nonce A))                          | decomp_r(14)
 * 16: known (Nonce B)                                        | decomp_l(15)
 * 17: known (C (Name I) (C (Nonce B) (Nonce A)))             | compose(6, 15)
 * 18: known (Enc A (C (Name I) (C (Nonce B) (Nonce A))))     | crypt(A, 17)
 * 19: send I (Enc A (C (Name I) (C (Nonce B) (Nonce A))))    | intruder(18)
 * 20: receive A (Enc A (C (Name I) (C (Nonce B) (Nonce A)))) | bcast(19, A)
 * 21: send A (Enc I (Nonce B))                               | msg3(20)
 * 22: receive I (Enc I (Nonce B))                            | bcast(21, I)
 * 23: known (Enc B (Nonce B))                                | crypt(B, 16)
 * 24: send I (Enc B (Nonce B))                               | intruder(2)
 * 25: receive B (Enc B (Nonce B))                            | bcast(24, B)
 * 26: bad_hs A B                                             | _bhs(2, 10, 20, 25)
 * 27: flaw [for X = A and Y = B]                             | 26, 5, 16
 *)

Answer 1

You can use assert to assert intermediate facts like the sequence of statements in your informal proof.

Theorem flaw : exists X Y, bad_hs X Y /\ known (Nonce X) /\ known (Nonce Y).
Proof.
  assert (F1 : send A (Enc I (C (Name A) (Nonce A)))).
  { apply msg1. eauto. }
  assert (F2 : receive I (Enc I (C (Name A) (Nonce A)))).
  { eapply bcast. eauto. }
(* etc. *)

Since each step uses really simple logic (apply constructor, apply assumptions or some basic propositional reasoning for the _ \/ _), you can condense them in a single tactic with the assert _ by _ variant, and eauto using _.

  assert (F1 : send A (Enc I (C (Name A) (Nonce A))))    by eauto using msg1.
  assert (F2 : receive I (Enc I (C (Name A) (Nonce A)))) by eauto using bcast.