isabelle update -u control_cartouches;

more symbols;

standardized towards new-style formal comments: isabelle update_comments;

session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;

proper latex setup;

more symbols;

isabelle update_cartouches -c -t;

modernized header uniformly as section;

updated news

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries

adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'

updated comment;

modernized specifications;

explicit file specifications -- avoid secondary load path;

updated some headers;

convert TLS to use Nat_Bijection library

replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)

eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;

Moved Nat_Int_Bij into Library

--HG--
rename : src/HOL/Nat_Int_Bij.thy => src/HOL/Library/Nat_Int_Bij.thy

Replaced Library/NatPair by Nat_Int_Bij.

Adapted to new inductive definition package.

more robust syntax for definition/abbreviation/notation;

replaced syntax/translations by abbreviation;

migrated theory headers to new format

Tidying and replacement of some axioms by specifications

improved presentation of HOL/Auth theories

Changes required by the certified email protocol

Public-key model now provides separate signature/encryption keys and also
long-term symmetric keys.

tidying of Isar scripts

tuned parentheses in relational expressions;

conversion of Auth/TLS to Isar script

misc tidying; changing the predicate isSymKey to the set symKeys

Some X-symbols for <notin>, <noteq>, <forall>, <exists>
Streamlining of Yahalom proofs
Removal of redundant proofs

tidying in conjuntion with the TISSEC paper; replaced (unit option)
by a new datatype (role)

changed tags from 0, 1 to None, Some() to avoid special treatment of 0

Got rid of not_Says_to_self and most uses of ~= in definitions and theorems

Tidying

Trivial change to be more like paper

Simplified SpyKeys and ClientKeyExch as suggested by James Margetson

Fixed spelling error

Fixed ServerResume to check for ServerHello instead of making a new NB

Exchanged the M and SID fields of the FINISHED messages to simplify proofs

Client, Server certificates now sent using the separate Certificate rule,
simplifying ServerHello and ClientKeyExch. Resumption no longer needs its
own version of ServerHello. Proofs run nearly three minutes faster.

Renamed XA, XB to PA, PB and removed the certificate from Client Verify

Deleted obsolete axioms inj_serverK and isSym_serverK

sessionK now indexed by nat instead of bool.
Weaker Oops conditions on final guarantees

Simplified SpyKeys to use sessionK instead of clientK and serverK
Proved and used analz_insert_key, shortening scripts

First working version with Oops event for session keys

Full version of TLS including session resumption, but no Oops

Global change: lost->bad and sees Spy->spies
First change just gives a more sensible name.
Second change eliminates the agent parameter of "sees" to simplify
definitions and theorems

Now with the sessionK constant and new events ClientAccepts and ServerAccepts

Addition of SessionIDs to the Hello and Finished messages

TLS now with a distinction between premaster secret and master secret

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.

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

New proofs involving CERTIFICATE VERIFY

New constant "certificate"--just an abbreviation

More realistic model: the Spy can compute clientK and serverK

Baby TLS. Proofs work, but model seems unrealistic