26 sep 2002
	- private identifiers in 'session*' declaration had to
be at least one.  We can now declare 'sessions *{}' or even just 'session *'
when no identifier should be private to all sessions.

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.

12 jul 2002
	- Corrected semantic bug in EVA parser.  Until now,
when you declared some function, e.g.

	shr (principal) : key secret hash

you probably meant to use shr as some way of allowing
principals A to compute some shared key shr(A) that
only them could compute (not the intruder, hence the
'secret' keyword), and that cannot be used to get back
at their identities (hence the 'hash' keyword).
	Unfortunately, this was basically taken as
the declaration of a *variable* shr of type principal -> key.
This in particular means that no two principals were forced
to store the same function under the name shr.
	While this is not in general a problem for shr, it
is in the case of public/private key pairs.  Assume you
type:

	keypair^alg PK, SK (principal, principal)

You probably mean that PK(A) should be A's public key,
while SK(A) should be A's private key.  This is all fine
until you realize that when some other principal B gets
A's identity, computing PK(A) does not need to return the
same result when it is computed by B or by A.
	This is visible in the parser because you cannot
state any property on PK(A): the parser complains you
didn't tell it which participant's PK function it is.

	This is corrected by having a new modifier for
variables: the new keyword 'shared'.  You may now declare
variables as before:
	A : principal
meaning that each principal may have a different idea
of what the value of A is really (recommended), or
	A : principal shared
meaning that each principal will be forced to have the
same value for A.  Note that using this may hide
security bugs; in particular, no check is being done in
the parser that, e.g., the value of A is not transmitted
along communication channels---if A is transmitted, there
is no reason the value received would match the value
sent in the Dolev-Yao model.

	Variables of functional types, such as shr, PK
or SK above are always declared shared.  I once wanted
to let the user choose whether (s)he wanted possibly unshared
functions, but decided against it, because it would incur
complex changes to the parser and I was not convinced that
it was useful at all.  Note in particular that it is impossible
to send functions on communication links, as only messages
can be sent, and no coercion function exists from functions
to messages---so it is impossible to code a protocol where
you would send one function f on one side, receive another one
on the other side, and had to care that both f's may be
different.

	The EVA parser is now happy with properties involving
PK(A)... provided you tell it which A it is, of course!

	This does not change anything in the semantics of
PEVA.  The changes above are meant to be upwards-compatible,
so that earlier LAEVA descriptions still compile without change.

11 jul 2002
	- Corrected bug in EVA parsing: in eva.y/yyerror(),
a global theSpecLineno was used to report line numbers at
which errors occurred.  This didn't take care of file
inclusions, notably.  yyerror() now uses yylloc, which
should be correct; theSpecLineno does not exist any longer.
	- added T_TYPE_SHARED to eva.y (cont'd: see 12 jul 2002)

19 mar 2002
	- Corrected bug in trans.ml/decompose_patterns and
in Doc/converge.tex: patterns apply(...) and secret-apply(...)
had been forgotten.
	Changed converge.tex so that intruder cannot apply
[hash-]apply-privk (this would defeat the very purpose of
private keys...)

17 mar 2002
	- Added 'secret' keyword in function declarations.
A secret function is meant not to be known to the intruder.
While this is useful in certain cases, e.g. to state the
existence of a function shr(principal):key such that the
intruder cannot reconstruct shr(A) when he knows A, it
is dangerous to use too liberally.  After all, a secret
function basically implements a covert channel---what we
are all after in cryptographic protocol design.

20 feb 2002
	- Added 'everybody knows' declaration to
concrete syntax.  Added structure 'everybody'
to trans.ml to handle things known to everybody.
Coercions created by 'basetype' are made known
to everybody: this corrects a bug in the version
of 04 feb 2002.

04 feb 2002
	- Added 'basetype' to syntax of Terms.
This creates a new base type, say <T>, and two
coercions '*<T>_of_D* : *D* -> <T>',
'*number_of_<T>* : <T> -> number'.
	Also, this allows one to create new objects
of type <T>.  In general now, we may create any
new object of type anything that can be coerced
from '*D*'.  This includes '*D*', 'number', and all
basetypes.
	The use of basetypes is discouraged.
However, this is necessary for tools like Yassine's,
Veronique's, or my own old CPV tool, which rely
on recognizing that a given message is not just
any number, rather a message of a specific basic
subtype ('key', 'nonce', etc.)  This is discouraged
because this simply ignores many attacks based
on type confusion.
	One standard basetype is defined in evalib.h,
'key'.  Note that it is defined as 'number' by default,
and you have to define the C preprocessor symbol
'BASETYPE_HACK' to activate 'key' as a genuine basetype.
This can be done by launching the parser 'evatolisp'
with the option '-DBASETYPE_HACK'.
	The nice thing is that, provided a protocol
includes 'evalib.h', nothing has to be changed in its
description when we wish to switch over from one
definition of 'key' to the other.  In particular,
appropriate coercions are inserted automatically in
case 'key' is a basetype.
	A final note: 'keypair' still generates pairs
of inverse keys of type 'number', not 'key'.  It is
unclear whether this should be changed.

01 feb 2002
	- Added 'located' to syntax of Terms in
subsection "Grammar" (\label{sec:abs:gram}).  Was
forgotten.

27 nov 2001
	- Started this file.
	- First distrib on 16 nov 2001.
	- Changes wrt. first distrib:
	  . signature matching was wrong: matching
on [M]_K once assumed receiver should never decrypt,
should only produce "exact" pattern on {M}_K.  This
is the opposite: receiver should always decrypt.
Solution taken: [M]_K is exactly synonymous with {M}_K.
The justification of two syntaxes for the same concept
is for documentation purposes (specifies the intent of
the specifier).
	  . added set of unknown data wrt. each role,
symmetrical to known data.  This allows evatrans to
detect more unimplementable messages.  For example,
	1. A -> B : {M}_K
	2. B -> A : M
where K is unknown to B, is now declared unimplementable
because B cannot get back the value that A intended to
hand him.