Require PolyList. Require knows. Section Gong. Variable B : Set. Inductive etatA : Set := etatA1 : etatA (* A a l'etape 1 *) | etatA4 : (msg B) -> etatA (* A a l'etape 4, contient la valeur de Na *) | etatA5 : (msg B) -> (msg B) -> etatA (* contient Kab, Nb2 *) | etatA6 : (msg B) -> etatA (* contient Kab *) . Inductive etatB : Set := etatB1 : etatB (* B a l'etape 1 *) | etatB2 : (msg B) -> (msg B) -> etatB (* contient idA, Na *) | etatB3 : (msg B) -> (msg B) -> (msg B) -> etatB (* contient idA, Na, Nb *) | etatB4 : (msg B) -> (msg B) -> (msg B) -> etatB (* contient Na, Kab, message_pour_A *) | etatB5 : (msg B) -> (msg B) -> etatB (* contient Kab, Nb2 *) | etatB6 : (msg B) -> etatB (* contient Kab *) . Inductive etatS : Set := etatS2 : etatS (* S a l'etape 2 *) | etatS3 : (msg B) -> (msg B) -> (msg B) -> (msg B) -> etatS (* contient Na, idA, Nb, idB *) | etatS4 : (msg B) -> (msg B) -> (msg B) -> (msg B) -> (msg B) -> etatS (* contient Na, idA, Nb, idB, Kab *) . Inductive etatglobal : Set := etat : etatA -> etatB -> etatS -> (list (msg B)) -> etatglobal. Variable idA, idB, kas, kbs : B. Inductive exec_1 : etatglobal -> etatglobal -> Prop := XA1 : (b:etatB) (s:etatS) (e:(list (msg B))) (na:B) (fresh e (base na)) -> (exec_1 (etat etatA1 b s e) (etat (etatA4 (base na)) b s (cons (pair (base idA) (base na)) e))) | XA2 : (b:etatB) (s:etatS) (e:(list (msg B))) (vna:(msg B)) (kab,nb2:B) (knows e (pair (crypt (pair vna (pair (base idB) (base kab))) (base kas)) (pair (crypt vna (base kab)) (base nb2)))) -> (exec_1 (etat (etatA4 vna) b s e) (etat (etatA5 (base kab) (base nb2)) b s e)) | XA3 : (b:etatB) (s:etatS) (e:(list (msg B))) (vkab,vnb2:(msg B)) (exec_1 (etat (etatA5 vkab vnb2) b s e) (etat (etatA6 vkab) b s (cons (crypt vnb2 vkab) e))) | XB1 : (a:etatA) (s:etatS) (e:(list (msg B))) (ida,na:B) (knows e (pair (base ida) (base na))) -> (exec_1 (etat a etatB1 s e) (etat a (etatB2 (base ida) (base na)) s e)) | XB2 : (a:etatA) (s:etatS) (e:(list (msg B))) (vida, vna:(msg B)) (nb:B) (fresh e (base nb)) -> (exec_1 (etat a (etatB2 vida vna) s e) (etat a (etatB3 vida vna (base nb)) s (cons (pair vna (pair vida (pair (base nb) (base idB)))) e))) | XB3 : (a:etatA) (s:etatS) (e:(list (msg B))) (vida, vna, vnb:(msg B)) (kab:B) (msg:(msg B)) (knows e (pair (crypt (pair vnb (pair vida (base kab))) (base kbs)) msg)) -> (exec_1 (etat a (etatB3 vida vna vnb) s e) (etat a (etatB4 vna (base kab) msg) s e)) | XB4 : (a:etatA) (s:etatS) (e:(list (msg B))) (vna,vkab,msg:(msg B)) (nb2:B) (fresh e (base nb2)) -> (exec_1 (etat a (etatB4 vna vkab msg) s e) (etat a (etatB5 vkab (base nb2)) s (cons (pair msg (pair (crypt vna vkab) (base nb2))) e))) | XB5 : (a:etatA) (s:etatS) (e:(list (msg B))) (vkab,vnb2:(msg B)) (knows e (crypt vnb2 vkab)) -> (exec_1 (etat a (etatB5 vkab vnb2) s e) (etat a (etatB6 vkab) s e)) | XS1 : (a:etatA) (b:etatB) (e:(list (msg B))) (vna,vida,vnb,vidb:(msg B)) (knows e (pair vna (pair vida (pair vnb vidb)))) -> (exec_1 (etat a b etatS2 e) (etat a b (etatS3 vna vida vnb vidb) e)) | XS2 : (a:etatA) (b:etatB) (e:(list (msg B))) (vna,vida,vnb,vidb:(msg B)) (kab:B) (fresh e (base kab)) -> (exec_1 (etat a b (etatS3 vna vida vnb vidb) e) (etat a b (etatS4 vna vida vnb vidb (base kab)) (cons (pair (crypt (pair vnb (pair vida (base kab))) (base kbs)) (crypt (pair vna (pair vidb (base kab))) (base kas))) e))). Inductive exec : etatglobal -> etatglobal -> Prop := X0 : (s:etatglobal) (exec s s) | X1 : (s1,s2,s3:etatglobal) (exec_1 s1 s2) -> (exec s2 s3) -> (exec s1 s3). Lemma correct_1 : (e0,e:(list (msg B))) (b0,b:etatB) (s0,s:etatS) (vkab:(msg B)) ~(knows e0 (base kas)) -> ~(knows e0 (base kbs)) -> (exec (etat etatA1 b0 s0 e0) (etat (etatA6 vkab) b s e)) -> ~(knows e vkab). End Gong.