Bug!: toutes les fonctions [hash-][secret-]apply supposent dans les regles
	de l'intrus que les arguments sont des messages (number).  Mais
	les regles de typage ne disent pas ca du tout.  Comment faire?

Bug?: quand on dit que S.Kbs est secret au debut d'une session,
	est-ce que ca veut dire au moment ou S recoit Kbs? ou vraiment au debut?
	Dans le premier cas, je ne vois pas comment j'ai pu decrire ca
	dans la semantique.  Dans le second, ca ne fournit aucune hypothese
	interessante. Je viens de regarder, c'est la seconde. Ca serait sympa
	que le typage detecte ca comme un probleme, au moins.  Quant a pouvoir
	specifier qu'un Kbs recu a une etape, disons 3, soit secret, comment
	faire?  (On peut quantifier sur les futurs: AG secret (Kbs)...)
Bug: shr(principal):key idiot car l'intrus va pouvoir creer tous les shr(A).
	Declarer shr private et dire dans la semantique de l'intrus que
	l'intrus ne sait pas appliquer les fonctions private.
	Note: les *apply-privk devraient etre private.
Bug: dans la semantique, new x doit creer x non kapprox dans E.
Bug: dans session *{Kas, Kbs} si Kas et Kbs sont des alias, ca ne va pas.
Note: (V. Cortier)
	A -> S : {B, A, Na}_Kas
	S -> B : {A, Na}_Kbs
	pose le probleme que comme Kbs est calcule comme shr (B),
ou B est recu par S.  Or il n'y a aucune hypothese permettant de conclure
que shr(B) est secrete.
	Je propose de declarer assume secret (shr (B@s1.A)), mais
Veronique dit que ca ne marche pas.  Il serait peut-etre meilleur que
shr(x) soit connu d'un principal que si x est une de ses identites.
Mene a la notion de fonction partiellement connue, voir Hubert.
Note: (Y. Lakhnech) ca serait bien de rajouter secret (M, ens-de-principaux-autorises).
	Yassine pense que la technique de Dominique est une approximation
superieure mais vissee dans le modele, et probablement trop crue.
Bug: keypair^alg autorise pour alg : sym_alg -> interdire.
Note: si on recoit {N}_K indechiffrable, puis plus tard K, on peut maintenant recuperer
	K.  Traducteur: pouvoir exprimer ce dechiffrement tardif par un B: X:=e ?
Bug: ... -> B : {PK (B)}_{PK (B)^alg}
	...
     ... -> B : {X}_{PK (B)^alg}
Note: dans semantique, "f in dom Inv" confusing -> "F in dom Inv" par ex.

Axiomes: on peut vouloir ecrire {...}_K % X pour forcer le recepteur a ne
	pas dechiffrer -> la verification d'egalite doit devenir une
	verification de E-matching.

Syntaxe: autoriser {...}^alg_K aussi bien que {...}_K^alg.

Axiomes: ne peuvent pas encore utiliser de variables quantifiees;
	gerer les axiomes par cc dans evatrans.
Faire session.role.expression

Ajoute declaration 'A, B : alias x=t' permet de declarer un alias local a A et a B.
Pb: si on veut declarer A.Na==B.Nb, aujourd'hui il faut ecrire equals(A,Na,B,Nb)
    mais ceci ne prend pas en compte les alias locaux.

Si dans nspub.eva on ne declare pas l'algorithme de chiffrement,
ni qu'il est asymetrique, on obtient une erreur etrange:
evatrans: nspub.eva, line 16(4)-16(20): non-implementable message, sender cannot build 'A'
C'est au message 4.  Or au message 3 B a recu {Na, A}_(PK(B)).
Mais bien sur si l'algorithme n'est pas declare, evatrans pense qu'il
est symetrique, donc il abstrait tout le pattern par une variable;
en particulier il ne connait ni Na ni A -> besoin de pretty-printer les processus
fabriques par evaparse pour verification.

keypair peut maintenant prendre un optional_encryption_algorithm (en fait, il le doit:
	(vanilla) est un algorithme symetrique, et ne peut pas definir de keypair).
dans la syntaxe abstraite,
	keypair
	asymk1, asymk2, lambda-pubk, lambda-privk, hash-apply-pubk, apply-pubk, hash-apply-privk, apply-privk
	prennent maintenant un premier argument d'algorithme en plus.
Le type algo est maintenant subdivise en deux sous-types sym_algo et asym_algo, avec coercions sa et aa.
(vanilla) devient (sa (vanilla)) dans la syntaxe abstraite de sortie.
algo devient *algo* (on ne peut plus declarer un algorithme sans dire s'il est symetrique ou non).

Proposition:
	virer le type key, ainsi que le constructeur k de la syntaxe abstraite.
	keypair creerait alors deux donnees de base (type *D*), on aurait asymk1, asymk2 : *D* -> number.
	Les newK seraient supprimes, remplaces par des new ordinaires de type *D*.
La ligne 549 (trans.ml; new de type *K*) : a reflechir.

Plein de petits details changes par rapport a la spec de Florent.
Ajoute des accolades autour des listes de messages, sinon shift/reduce conflit.
%session a:A plutot que A=a
A knows ... : stupide, c'est plutot a knows (l'instance, pas le role)
comment differencie-t-on les sessions entre elles ?
que veut dire hash ?  non inversible, oui, mais au sens mathematique, ou par l'intrus ?
	-> non inversible par l'intrus

syntaxe keypair enrichie: keypair PK, SK (principal)
noms optionnels de sessions ajoutes
ajoutees les signatures, syntaxe [M]_K

TODO:
%Ajouter session A=I -> A est declare intrus, et aucun processus
%n'est compile par le translateur.

BUGS:
%dans nspub.cpl, cree pattern hash-apply-pubk (impossible).
dans nspriv.eva, S_key_base (principal, principal) : key parse sans erreur (?)

%%dans dh.cpl, 'a.A cree deux fois *P*new_base*