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

(** A simple cryptographic protocol for paid TV *)

(** ** Basic data types *)

(** - Users;
     - Agents : C is the smartcard, D is the decoder 
     parameterized by the user and I is the intruder;
     - Keys and data: keys will be symmetric and private;
     - Messages: the keys, or data or names of agents, 
   messaged can be encoded and paired.
*)

Variable user : Set.

Inductive agent : Set := C : user->agent | D : user->agent | I .

Variables key data : Set.

(* TO BE COMPLETED *)
Inductive message : Set := 
	Name  : agent -> message (* names of agents *)
      | K   : (* keys *)
      | Data :  (* datas *)
      | Enc :  (* encrypted messages *)
      | P  : (* pair of messages *)

(** - Property (known by the smartcard) which says that 
   the fees for accessing the data has been paid.*)

Variable paid : user -> Prop.

(** ** Description of the protocol *)

(** The protocol is parameterized by the messages 
[m1] and [m2] to be exchanged.

Three mutually inductively defined relations:
 -[send A m] when [A] send a message [m]
   encodes the protocol 
    -- D n --> C n : (D n,m1)
    -- C n --> D n : (C n,m2) if paid n

The intruder [I] can send any message that (s)he knows;
 -[receive B m] when [B] 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],
   it is the names of an agent
   or deducible from informations received by [I] 
      - [I] can form and break pairs 
                encode/decode messages when key is known
*)

Section Protocol.

Variables m1 m2: message.

Inductive send  : agent -> message -> Prop :=
     init   : forall n, send (D n) (P (Name (D n)) m1)
   | trans1 : forall n, receive (C n) (P (Name (D n)) m1)
              -> paid n -> send (C n) (P (Name (C n)) m2)
   | cheat : forall m, known m -> send I m

with receive : agent -> message -> Prop :=
     link : forall m A B, send A m -> receive B m

(* TO BE COMPLETED *) 
with known : message -> Prop :=

.


(** - The protocol ends when the decoder [D n] 
   receives the message [(P (Name (C n)) m2)].
*)

Definition ok n : Prop := receive (D n) (P (Name (C n)) m2).

End Protocol.

Hint Unfold ok.
Hint Resolve init trans1 link decomp_l decomp_r compose cheat spy name.

(** - If the fee has been paid then the protocol ends successfully
       whatever the messages are. *)

Lemma paid_get : forall m1 m2 n, paid n -> ok m1 m2 n.
(* TO BE COMPLETES *)

Save.


(**
   - If the two messages [m1] amd [m2] are the same, and 
   the intruder knows the name of the smartcard,
   then the protocol can be executed even 
   when the fee was not paid.
*)

Lemma flaw : forall n m, ok m m n.
(* TO BE COMPLETED *)
Save.

(** ** Instantiated version *)

Variable k : key.

Variables d1 d2:data.

Definition m1 := Enc (Data d1) k.
Definition m2 := Enc (Data d2) k.


(** ** Properties of the protocol *)


(** - no flaw when nobody paid. *)
Section no_flaw_section.

Hypothesis no_paid : forall n, ~ paid n.

Scheme receive_mut_ind := Minimality for receive Sort Prop 
with known_mut_ind := Minimality for known Sort Prop 
with send_mut_ind := Minimality for send Sort Prop.

(** Print/Check receive_mut_ind *)

(** - Invariant : approximate what is known from the intruder. *)

(* TO BE COMPLETED *)
Inductive invknown :  message -> Prop := 
.  

Hint Constructors invknown.

Lemma receive_invknown : forall a m, receive m1 m2 a m -> invknown m.
intros.
elim H using receive_mut_ind 
       with (P0 := invknown) 
              (P1 := fun a:agent => invknown); 
       intros; auto.
(* TO BE COMPLETED *)

Save.

Hypothesis d1_not_d2 : ~d1=d2.

Lemma invknown_not_ok : forall n, ~ invknown (P (Name (C n)) m2).
(* TO BE COMPLETED *)

Save.


Lemma no_flaw : forall n, ~ ok m1 m2 n.
(* TO BE COMPLETED *)

End no_flaw_section.

(** - Flaw: if somebody paid then everybody is ok. *)
Section flaw_section2.
Variable p:user.
Hypothesis p_paid : paid p.

Lemma flaw2 : forall n, ok m1 m2 n.
(* TO BE COMPLETED *)

Save.

Print flaw2.
End flaw_section2.