Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* 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.