src/HOL/Auth/Auth_Shared.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 32632 8ae912371831
child 61830 4f5ab843cf5b
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Copyright   1996  University of Cambridge
     3 *)
     4 
     5 section {* Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols *}
     6 
     7 theory Auth_Shared
     8 imports
     9   "NS_Shared"
    10   "Kerberos_BAN"
    11   "Kerberos_BAN_Gets"
    12   "KerberosIV"
    13   "KerberosIV_Gets"
    14   "KerberosV"
    15   "OtwayRees"
    16   "OtwayRees_AN"
    17   "OtwayRees_Bad"
    18   "OtwayReesBella"
    19   "WooLam"
    20   "Recur"
    21   "Yahalom"
    22   "Yahalom2"
    23   "Yahalom_Bad"
    24   "ZhouGollmann"
    25 begin
    26 
    27 end