src/HOL/Auth/Auth_Public.thy
author wenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070 b72a990adfe2
parent 58889 5b7a9633cfa8
child 61830 4f5ab843cf5b
permissions -rw-r--r--
prefer symbols;
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@58889
     5
section {* Conventional protocols: rely on conventional Message, Event and Public -- Public-key protocols *}
paulson@1944
     6
haftmann@32632
     7
theory Auth_Public
haftmann@32632
     8
imports
haftmann@32632
     9
  "NS_Public_Bad"
haftmann@32632
    10
  "NS_Public"
haftmann@32632
    11
  "TLS"
haftmann@32632
    12
  "CertifiedEmail"
haftmann@32632
    13
begin
paulson@14145
    14
haftmann@32632
    15
end