tuned warning;

tuned warning; renamed |-> <-| <-> to Parse/PrintRule;

improved output channels: normal, warning, error;

fixed EqI meta rule;

changes needed for introducing fairness

changes neede for introducing fairness

changes needed for adding fairness

fixed merge of internal simprocs;

Changing "lost" from a parameter of protocol definitions to a constant. Advantages: no "lost" argument everywhere; fewer Vars in subgoals; less need for specially instantiated rules Disadvantage: can no longer prove "Agent_not_see_encrypted_key", but this theorem was never used, and its original proof was also broken the introduction of the "Notes" constructor.

Fixed delIffs to deal correctly with the D-rule

Removed redundant addsimps of Un_insert_left, which is now a default simprule

Removal of monotonicity reasoning involving "lost" and the theorem Agent_not_see_encrypted_key, which (a) is never used and (b) becomes harder to prove when Notes is available.

Now uses the Notes constructor to distinguish the Client (who has chosen M) from the Spy (who may have replayed her messages)

Moved some declarations to Message from Public and Shared

Now loads theory Event, which contains common declarations

Moving common declarations and proofs from theories "Shared" and "Public" to "Event". NB the original "Event" theory was later renamed "Shared". Addition of the Notes constructor to datatype "event".

removed obsolete init_pps and init_thy_reader;

improved type checking errors;

removed init_pps;

removed init_database;

Improved length = size translation.

New proofs involving CERTIFICATE VERIFY

eliminated chmod -w;

-w option;

NOWRITE;

added -w option;

Changed some variables of type msg to lower case (e.g. from NB to nb

New constant "certificate"--just an abbreviation

Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).

Automatic update