History log of /seL4-l4v-master/l4v/isabelle/src/HOL/Auth/CertifiedEmail.thy
Revision Date Author Comments
# ed7a971e 05-Jan-2019 wenzelm <none@none>

isabelle update -u control_cartouches;


# f5796e6d 14-Feb-2018 wenzelm <none@none>

more symbols;


# 5385dbfa 16-Jan-2018 wenzelm <none@none>

standardized towards new-style formal comments: isabelle update_comments;


# ce5e1da3 28-Dec-2015 wenzelm <none@none>

more symbols;


# feca4ab8 10-Dec-2015 wenzelm <none@none>

isabelle update_cartouches -c -t;


# 794edf80 02-Nov-2014 wenzelm <none@none>

modernized header uniformly as section;


# e98d2ce8 28-Jun-2011 paulson <none@none>

simplified proofs using metis calls


# deac04eb 22-Jul-2010 wenzelm <none@none>

updated some headers;


# baea5702 01-Mar-2010 haftmann <none@none>

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


# 079cde2d 17-Oct-2009 wenzelm <none@none>

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


# 7b63d2a6 11-Jul-2007 berghofe <none@none>

Adapted to new inductive definition package.


# cd65d9bc 16-Nov-2006 wenzelm <none@none>

more robust syntax for definition/abbreviation/notation;


# 8d37dcbe 28-Sep-2006 wenzelm <none@none>

replaced syntax/translations by abbreviation;


# d84f4588 28-Sep-2005 paulson <none@none>

streamlined theory; conformance to recent publication


# a7060872 17-Jun-2005 haftmann <none@none>

migrated theory headers to new format


# e6988de0 20-Jul-2004 paulson <none@none>

minor tweaks to go with the new version of the Accountability paper


# 6467ec76 11-May-2004 paulson <none@none>

removal of prime characters


# 5442a36e 26-Sep-2003 paulson <none@none>

Conversion of all main protocols from "Shared" to "Public".
Removal of Key_supply_ax: modifications to possibility theorems.
Improved presentation.


# d66531ec 23-Sep-2003 paulson <none@none>

Removal of the Key_supply axiom (affects many possbility proofs) and minor
changes


# 05eb17d2 12-Aug-2003 paulson <none@none>

ZhouGollmann: new example (fair non-repudiation protocol)


# 7a4d9400 05-May-2003 paulson <none@none>

improved presentation of HOL/Auth theories


# d9407e84 28-Apr-2003 paulson <none@none>

better guarantees


# 63be96be 25-Apr-2003 paulson <none@none>

converting more HOL-Auth to new-style theories


# c5f9f5e4 25-Apr-2003 paulson <none@none>

Changes required by the certified email protocol

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