src/HOL/Auth/Smartcard/Auth_Smartcard.thy
author haftmann
Mon Sep 21 15:33:40 2009 +0200 (2009-09-21)
changeset 32632 8ae912371831
parent 28098 src/HOL/Auth/ROOT.ML@c92850d2d16c
child 58889 5b7a9633cfa8
permissions -rw-r--r--
added session entry point theories
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
haftmann@32632
     5
header {* 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