src/HOL/Auth/Smartcard/Auth_Smartcard.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;
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 {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
paulson@1944
     6
haftmann@32632
     7
theory Auth_Smartcard
haftmann@32632
     8
imports
haftmann@32632
     9
  "ShoupRubin"
haftmann@32632
    10
  "ShoupRubinBella"
haftmann@32632
    11
begin
paulson@14145
    12
haftmann@32632
    13
end