src/HOL/Auth/Auth_Shared.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 65538 a39ef48fbee0
permissions -rw-r--r--
tuned;
     1 (*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Copyright   1996  University of Cambridge
     3 *)
     4 
     5 section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close>
     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