# How do I prove this property in Coq?

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
*)

• I know you say the few tactics you know are insufficient, but have you at least done the proof with pen and paper? Do you know the main idea of the proof? Then you can ask about the steps you would like to do but don't know the tactics for. (In general, unless you know how to do a proof with pen and paper, you won't be able to do it formally. In formal math it is quite easy to loose the forest for the trees.) Aug 30 at 0:22
• Yes, I did (sort of). If it can help I can share it. Aug 30 at 3:35
• I added a sketch of the proof in the comments to the Coq code. Aug 30 at 8:38

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.

• Thank you; with assert _ by eauto using _ I managed to assert all the intermediate facts except for F26, that was slightly more complex to digest: assert (F26: bad_hs A B). { eapply _bhs. - eauto. - eauto. - discriminate. - eapply F2. - eapply F10. - eapply F20. - eapply F25. } Aug 31 at 12:23
• If you also assert A <> B and B <> A that should help eauto take care of that last case. Sep 1 at 1:44