src/HOL/Auth/Auth_Public.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;
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 -- Public-key protocols\<close>
paulson@1944
     6
haftmann@32632
     7
theory Auth_Public
haftmann@32632
     8
imports
wenzelm@65538
     9
  NS_Public_Bad
wenzelm@65538
    10
  NS_Public
wenzelm@65538
    11
  TLS
wenzelm@65538
    12
  CertifiedEmail
haftmann@32632
    13
begin
paulson@14145
    14
haftmann@32632
    15
end