src/HOL/Auth/Auth_Shared.thy
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 65538 a39ef48fbee0
permissions -rw-r--r--
tuned;
haftmann@32632
     1
(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1944
     2
    Copyright   1996  University of Cambridge
paulson@1944
     3
*)
paulson@1944
     4
wenzelm@61830
     5
section \<open>Conventional protocols: rely on conventional Message, Event and Public -- Shared-key protocols\<close>
paulson@1944
     6
haftmann@32632
     7
theory Auth_Shared
haftmann@32632
     8
imports
wenzelm@65538
     9
  NS_Shared
wenzelm@65538
    10
  Kerberos_BAN
wenzelm@65538
    11
  Kerberos_BAN_Gets
wenzelm@65538
    12
  KerberosIV
wenzelm@65538
    13
  KerberosIV_Gets
wenzelm@65538
    14
  KerberosV
wenzelm@65538
    15
  OtwayRees
wenzelm@65538
    16
  OtwayRees_AN
wenzelm@65538
    17
  OtwayRees_Bad
wenzelm@65538
    18
  OtwayReesBella
wenzelm@65538
    19
  WooLam
wenzelm@65538
    20
  Recur
wenzelm@65538
    21
  Yahalom
wenzelm@65538
    22
  Yahalom2
wenzelm@65538
    23
  Yahalom_Bad
wenzelm@65538
    24
  ZhouGollmann
haftmann@32632
    25
begin
paulson@14145
    26
haftmann@32632
    27
end