Veronique,

	bon j'ai quand meme pu travailler un petit peu sur EVA
durant les confs.
	J'ai donc modifie un tant soit peu la distrib EVA.
	Voici ce que j'ai fait, en reponse a tes questions.

1. pour Needham-Schroeder, ton probleme (il utilisait des cles
	prives au lieu de cles publiques pour dechiffrer, ou
	le contraire) etait que tu n'avais pas specifie le
	nom de l'algorithme de chiffrement.  Si tu ne le
	specifies pas, le parser suppose que tu utilises
	vanilla(), qui est un algorithme de chiffrement
	symetrique.  C'est parfaitement valide en EVA, mais
	alors pour dechiffrer un message chiffre avec une
	cle privee (par exemple), il faut utiliser la meme
	cle privee.
   Il n'y a aucune solution formelle pour empecher ca.  Par
contre, j'ai rajoute a traducteur une verification supplementaire:
le traducteur evatrans essaie de verifier que l'algorithme
de chiffrement utilise pour chiffrer/dechiffrer est compatible
avec la cle qu'on utilise.  Si ce n'est pas le cas, evatrans
affiche un warning (pas une erreur, c'en n'est peut-etre pas une.)

	Au passage, il faudra mettre un jour une option de commande
pour deconnecter ce genre de warnings, au cas ou quelqu'un le voudrait
un jour.

2. pour Yahalom6, le probleme c'etait que tu faisais comme je
	te l'avais recommande pour declarer la fonction shr() ;-).
   En resume, quand j'ai introduit les fonctions 'secret', j'avais
melange plusieurs notions, et le fait d'ecrire
	'everybody knows shr'
(avec 'shr (principal) : number secret')
voulait vaguement dire dans mon esprit que tout le monde avait
la meme idee de ce que 'shr' etait.
	Bon depuis on a eu ce probleme curieux qu'en fait A et B
insistaient pour avoir des versions a eux, possiblement differentes,
de la fonction 'shr'.  J'ai corrige ca en disant que la declaration
'shr (principal) : number secret' allait declarer 'shr' comme etant
commune a tout le monde (fichier history, 12 jul 2002).
	Du coup, il ne faut *pas* ecrire 'everybody knows shr'!
En fait, ca veut dire que tout le monde peut construire shr(X)
des qu'il connait X.
	En particulier dans ton exemple, on demande a A de recuperer
un message {A, Kab}_shr(B), mais bien sur si 'everybody knows shr'
est vrai alors comme A connait l'identite B, il connait shr(B), donc
il peut le dechiffrer.  Et ca n'est pas ce que tu voulais (moi non
plus).
	En fait, il faut virer le 'everybody knows' et ecrire:

  //everybody knows shr : non
  A knows shr(A)
  B knows shr(B)

	Bon, voila, j'espere que ca t'aidera.
	Bonnes vacances si tu en prends!

	-- Jean.



Les messages ajoutes en tete du fichier history:

27 jul 2002
	- added warning messages (in Translator/trans.ml)
so that using encryption or signing with some algorithm,
and with some key based on some other algorithm is flagged
as a warning.  Usually, this manifests itself when we write
	{M}_K
where K is some public or private key.  This is usually a
mistake, because encryption will be using algorithm (vanilla),
which is symmetric.  In particular, to decrypt {M}_K, the
translator will try to use K again, not its inverse.
	Note that no warning is issued when some key meant
for some *symmetric* encryption algorithm is used with another:
this is no anomaly, as the actual behaviour of the resulting
processes is unambiguous (decrypt with key K).

	- Added new piece of syntax to eva.y: we may now write
{M}^algo_K instead of {M}_K^algo (the only allowed syntax until now);
similarly for signatures.

16 jul 2002
	- corrected slight bug in typing shared variables.
I should have checked whether x is in sigma before I call
check_var to check whether this is a legal shared variable.
	- Bumped version of converge.tex to 7.