(* The agents : smartcard, the decoder and the intruder *)
Inductive agent : Set := C : nat->agent | D : nat->agent | I : agent.

(* Only one encoding key, symmetric and private *)

Variables key,data : Set.
Variable k : key.

Variables d1,d2:data.

(* The messages can be the keys, or data : agents or data, 
   they can be encoded and paired *)

Inductive message : Set := 
	Name  : agent -> message
      | K   : key -> message
      | Data : data -> message
      | Enc : message -> key -> message
      | P  : message -> message -> message.

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

Variable paid : nat -> Prop.

(* 
   send A m when A send a message m
   code le protocole 
   D n --> C n : (D n,m1)
   C n --> D n : (C n,m2)
   
The intruder I can send any message tha (s)he knows

   receive B m when A may receive the message m 
   (ie, the message was sent by someone)

   known m when the message m is known from I, ie he was intercepted by I 
   or deducible from informations received by I
*)
Section Protocole.

Variables m1,m2: message.

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

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

with known : message -> Prop :=
     spy : (m:message)(receive I m)->(known m)
   | name : (a:agent)(known (Name a))
   | decomp_l : (m1,m2:message)(known (P m1 m2))->(known m1)
   | decomp_r : (m1,m2:message)(known (P m1 m2))->(known m2)
   | compose  : (m1,m2:message)(known m1)->(known m2)->(known (P m1 m2))
   | crypt  : (m:message)
                (k:key)(known m)->(known (K k))->(known (Enc m k))
   | decrypt  : (m:message)
                (k:key)(known (Enc m k))->(known (K k))->(known m).

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

End Protocole.

(* The protocol ends when the decoder D n receives the message 
   (receive D (P (Name (C n)) m2))
*)


Hints Unfold ok.
Hints Resolve init trans1 link.

(* If the fee has been paid then the protocol may execute *)
Lemma paid_get : (m1,m2:message)(n:nat)(paid n) -> (ok m1 m2 n).
Red; Intros.
Apply link with (C n); EAuto.
Save.

Hints Resolve decomp_l decomp_r.
Hints Resolve compose cheat spy name.

(* 
   The protocol can be executed when the fee was not paid, 
   when the intruder knows the name of the smartcard.
*)

Lemma flaw : (n:nat)(m:message)(ok m m n).
Red; Intros.
Apply link with I; Auto.
Apply cheat; EAuto.
Existential 1 := n.
Save.

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

(** Invariant *)

Inductive invknown :  message -> Prop :=    
     base : (a:agent)(invknown (Name a))
   | mes  : (invknown m1)
   | invcompose  : (m1,m2:message)
                (invknown m1)->(invknown m2)->(invknown (P m1 m2)).
Hints Resolve base mes invcompose.

Section no_flaw_section.

Hypothesis no_paid : (n:nat)~(paid n).
Hypothesis d1_not_d2 : ~(d1=d2).


Lemma invknown_not_ok : (n:nat)~(invknown (P (Name (C n)) m2)).
Red; Intros.
Inversion H.
Inversion H3.
Apply d1_not_d2; Trivial.
Save.

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.

Lemma no_flaw : (n:nat)~(ok m1 m2 n).
Unfold ok; Red ; Intros.
Apply (invknown_not_ok n).
Elim H using receive_mut_ind 
       with P0 := invknown P1 := [a:agent][m:message](invknown m); 
       Intros; Auto.
Inversion H1; Trivial.
Inversion H1; Trivial.
Inversion H3.
Inversion H3.
Case (no_paid n0); Trivial.
Save.
End no_flaw_section.

Section flaw_section2.
Variable p:nat.
Hypothesis p_paid : (paid p).

Lemma flaw2 : (n:nat)(ok m1 m2 n).
Red;Intros.
Apply link with I.
Apply cheat.
Apply compose; Auto.
Apply decomp_r with (Name (C p)); EAuto.
Save.

End flaw_section2.