/* Le protocole de Gong:
    1. A -> B : A, Na
    2. B -> S : Na, A, Nb, B
    3. S -> B : {Nb, A, Kab}_{Kbs}, {Na, B, Kab}_{Kas}
    4. B -> A : {Na, B, Kab}_{Kas}, {Na}_{Kab}, Nb2
    5. A -> B : {Nb2}_{Kab}
*/

/* On definit un etat global du systeme
comme etant un quadruplet (etat-de-A, etat-de-B, etat-de-S, etat-de-l'intrus).

L'etat de l'intrus est modelise comme une liste de message que l'intrus a
obtenus (par lecture des lignes de communication, typiquement).

*/

/* On commence par traiter ce que fait A: */

/* Etape 1, emission:
L'etat de A avant est etatA(1), autrement dit A est en attente d'emission
a l'etape 1.
L'etat de A apres est etatA(4, base(Na)) : le 4 signifie que A est en
attente de reception a l'etape 4, et base(Na) enregistre la valeur du
nonce Na.
Ce nonce est cree neuf, en particulier pas connu par l'intrus avant,
et ce quelque soient les cles supplementaires que l'on pourrait donner
a l'intrus.  (On devrait coder ceci par un predicat new, mais a la
place on utilise la primitive gensym/2 de Prolog.)

L'etat de l'intrus avant est une inconnue E, et l'etat apres est
E auquel on a ajoute pair(base(idA), base(Na)), soit le message
envoye par A a B.

Les etats de B et de S avant (EtatB, EtatS) sont identiques aux
etats de B et de S apres.
*/

exec_1(etatglobal(etatA(1), EtatB, EtatS, E),
       etatglobal(etatA(4, base(Na)), EtatB, EtatS, [pair(base(idA), base(Na)) | E])) :-
	gensym(nonce,Na).
	/* not knows(E,base(Na)). */

/* A attend ensuite en etape 4 la reception d'un message de la forme indiquee.
Lorsque ceci arrive, A passe a l'etat 5 (attente d'emission), et enregistre
la valeur de la cle Kab obtenue, et la valeur du nonce Nb2 recu (normalement) de B.
*/

exec_1(etatglobal(etatA(4, ValueNa), EtatB, EtatS, E),
       etatglobal(etatA(5, base(Kab), base(Nb2)), EtatB, EtatS, E)) :-
	knows(E, pair(crypt(pair(ValueNa, pair(base(idB), base(Kab))), base(kas)),
                      pair(crypt(ValueNa, base(Kab)),
                           base(Nb2)))).

/* Enfin, A envoie le message de l'etape 5.
*/

exec_1(etatglobal(etatA(5, ValueKab, ValueNb2), EtatB, EtatS, E),
       etatglobal(etatA(6, ValueKab), EtatB, EtatS, [crypt(ValueNb2, ValueKab) | E])).

/* On traite le cas de B, maintenant: */

exec_1(etatglobal(EtatA, etatB(1), EtatS, E),
       etatglobal(EtatA, etatB(2, base(IdA), base(Na)), EtatS, E)) :-
	knows(E, pair(base(IdA), base(Na))).

exec_1(etatglobal(EtatA, etatB(2, ValueIdA, ValueNa), EtatS, E),
       etatglobal(EtatA, etatB(3, ValueIdA, ValueNa, base(Nb)), EtatS,
                  [pair(ValueNa, pair(ValueIdA, pair(base(Nb), base(idB)))) | E])) :-
	gensym(nonce,Nb).
	/* not knows(E,base(Nb)).*/

exec_1(etatglobal(EtatA, etatB(3, ValueIdA, ValueNa, ValueNb), EtatS, E),
       etatglobal(EtatA, etatB(4, ValueNa, base(Kab), Message_pour_A), EtatS, E)) :-
	knows(E, pair(crypt(pair(ValueNb, pair(ValueIdA, base(Kab))), base(kbs)),
                      Message_pour_A)).

exec_1(etatglobal(EtatA, etatB(4, ValueNa, ValueKab, Message_pour_A), EtatS, E),
       etatglobal(EtatA, etatB(5, ValueKab, base(Nb2)), EtatS,
                  [pair(Message_pour_A, pair(crypt(ValueNa, ValueKab), base(Nb2))) | E])) :-
	gensym(nonce,Nb2).
	/* not knows(E,base(Nb2)).*/

exec_1(etatglobal(EtatA, etatB(5, ValueKab, ValueNb2), EtatS, E),
       etatglobal(EtatA, etatB(6, ValueKab), EtatS, E)) :-
	knows(E, crypt(ValueNb2, ValueKab)).

/* Et finalement le cas de S (en mono-session) : */

exec_1(etatglobal(EtatA, EtatB, etatS(2), E),
       etatglobal(EtatA, EtatB, etatS(3, ValueNa, ValueIdA, ValueNb, ValueIdB), E)) :-
	knows(E, pair(ValueNa, pair(ValueIdA, pair(ValueNb, ValueIdB)))).

exec_1(etatglobal(EtatA, EtatB, etatS(3, ValueNa, ValueIdA, ValueNb, ValueIdB), E),
       etatglobal(EtatA, EtatB, etatS(4, ValueNa, ValueIdA, ValueNb, ValueIdB, base(Kab)),
                  [pair(crypt(pair(ValueNb, pair(ValueIdA, base(Kab))), base(kbs)),
                        crypt(pair(ValueNa, pair(ValueIdB, base(Kab))), base(kas))) | E])) :-
	gensym(cle,Kab).
	/* not knows(E, base(Kab)).*/

/* Le system evolue d'etat a etat un nombre fini quelconque de fois:
*/

exec(EtatAvant, EtatApres) :-
	exec_1(EtatAvant, EtatIntermediaire), exec(EtatIntermediaire, EtatApres).

exec(EtatFinal, EtatFinal).

/* Nous devons maintenant verifier que pour tout etat E0 de l'intrus au demarrage
d'une session, si base(kas) et base(kbs) sont indeductibles a partir de E0,
et si A arrive au bout de la session (en etat 6), alors ce sera dans un etat
E de l'intrus ou:
1. la valeur de Kab recuperee par A est indeductible de l'intrus dans l'etat E;
2. base(kas) et base(kbs) sont indeductibles de l'intrus dans l'etat E.

Et similairement pour B lorsqu'il arrive dans son etat 6.

En pratique, on va demander a Prolog les cas ou on a simultanement :
a. l'intrus dans l'etat E peut deduire la valeur de Kab telle que recuperee par A;
b. E est obtenu a la fin d'une session, E0 etant l'etat de l'intrus au debut de la session;
c. base(kas) et base(kbs) sont indeductibles de l'intrus dans l'etat E0.

Autrement dit:
exec(etatglobal(etatA(1), _, _, E0), etatglobal(etatA(6, ValueKab), _, _, E)),
knows(E, ValueKab),
not knows(E0, base(kas)),
not knows(E0, base(kbs))
.
*/