(** * Example of manipulation of inductive definitions *)

(** Needham-Schroeder protocol *)
(** simplified bversion without a server for distributing public keys *)

(** ** Basic data types *)
(** - Users;
    - Agents : A is Alice, B is Bob, I is the intruder
    - Keys and data: keys will be asymmetric and public;
    - Messages: the keys, or names of agents, 
      or nonces generated by one agent for another;
      messages can be encoded with the public key of an agent and paired.
*)

Inductive agent : Set := A | B | I .

Inductive message : Set := 
	Name  : agent -> message
      | Nonce : agent * agent -> message
      | SK    : agent -> message 
      | Enc   : message -> agent -> message
      | P     : message -> message -> message.

(** ** Description of the protocol *)

(** 
Three mutually inductively defined relations:
 - [send Y m] when [Y] send a message [m] encodes the protocol 
    -- A --> B : {NA,A} pk(B) 
    -- B --> A : {NA,NB} pk(A)
    -- A --> B : {NB} pk(B)
The intruder [I] can send any message that (s)he knows;
 - [receive Z m] when [Z] receive the message m 
   (ie, the message was sent by someone);
 - [known m] when the message [m] is known from [I], ie 
   it was intercepted by [I] or deducible from informations received by [I].
*)

Section Protocol_with_flaw.

(** A global parameter [X] represents the agent with which [A] initiates the protocol *)

Variable X:agent.

(** [A] and [B] follow the protocol *)

Inductive send : agent -> message -> Prop :=
     init   : send A (Enc (P (Nonce (A,X)) (Name A)) X)
   | trans1 : forall Y d, 
              receive B (Enc (P (Nonce d) (Name Y)) B)
              -> send B (Enc (P (Nonce d) (Nonce (B,Y))) Y)
   | trans2 : forall d, receive A (Enc (P (Nonce (A,X)) (Nonce d)) A)
              -> send A (Enc (Nonce d) X)
   | cheat : forall m, known m -> send I m

with receive : agent -> message -> Prop :=
     link : forall m Y Z, send Y m -> receive Z m

with known : message -> Prop :=
     spy : forall m, receive I m -> known m
   | name : forall a, known (Name a)
   | nonce : forall Y, known (Nonce (I,Y))
   | secret_KI : known (SK I)
   | decomp_l : forall m m', known (P m m') -> known m
   | decomp_r : forall m m', known (P m m') -> known m'
   | compose  : forall m m', known m -> known m' -> known (P m m')
   | crypt  : forall m a, known m -> known (Enc m a)
   | decrypt : forall m a, known (Enc m a) -> known (SK a) -> known m.


End Protocol_with_flaw.
Hint Resolve init trans1 link secret_KI
             decomp_l decomp_r compose cheat spy name.

(** The protocol can end with [B] receiving the message [(Enc (Nonce (B,A)) B)]
    while the protocol was initiated with [I].
*)

Lemma flaw : receive I B (Enc (Nonce (B,A)) B).
apply link with I.
apply cheat.
apply crypt; auto.
apply decrypt with I; auto.
apply spy.
apply link with A.
apply trans2.
apply link with I.
apply cheat.
apply spy.
apply link with B.
apply trans1.
apply link with I.
apply cheat.
apply crypt; auto.
apply decrypt with I; auto.
apply spy.
apply link with A.
apply init.
Qed.

(** The nonce generated by [B] for [A] is made public *)

Lemma flawB : known I (Nonce (B,A)).
apply decrypt with I; auto.
apply spy.
apply link with A.
apply trans2.
apply link with I.
apply cheat.
apply spy.
apply link with B.
apply trans1.
apply link with I.
apply cheat.
apply crypt; auto.
apply decrypt with I; auto.
apply spy.
apply link with A.
apply init.
Qed.