src/HOL/Auth/Smartcard/Auth_Smartcard.thy
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 32632 8ae912371831
child 58889 5b7a9633cfa8
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32632
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
     1
(*  Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1944
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
     2
    Copyright   1996  University of Cambridge
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
     3
*)
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
     4
32632
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
     5
header {* Smartcard protocols: rely on conventional Message and on new EventSC and Smartcard *}
1944
ea0f573b222b ROOT file for Auth directory
paulson
parents:
diff changeset
     6
32632
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
     7
theory Auth_Smartcard
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
     8
imports
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
     9
  "ShoupRubin"
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
    10
  "ShoupRubinBella"
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
    11
begin
14145
2e31b8cc8788 ZhouGollmann: new example (fair non-repudiation protocol)
paulson
parents: 13922
diff changeset
    12
32632
8ae912371831 added session entry point theories
haftmann
parents: 28098
diff changeset
    13
end