src/HOL/Auth/Smartcard/Auth_Smartcard.thy
author wenzelm
Thu Dec 10 21:39:33 2015 +0100 (2015-12-10)
changeset 61830 4f5ab843cf5b
parent 58889 5b7a9633cfa8
child 65538 a39ef48fbee0
permissions -rw-r--r--
isabelle update_cartouches -c -t;
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>Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard\<close>
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