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.