--- a/src/HOL/Auth/CertifiedEmail.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy Thu Sep 28 23:42:35 2006 +0200
@@ -7,13 +7,12 @@
theory CertifiedEmail imports Public begin
-syntax
- TTP :: agent
- RPwd :: "agent => key"
+abbreviation
+ TTP :: agent
+ "TTP == Server"
-translations
- "TTP" == "Server "
- "RPwd" == "shrK "
+ RPwd :: "agent => key"
+ "RPwd == shrK"
(*FIXME: the four options should be represented by pairs of 0 or 1.
--- a/src/HOL/Auth/Event.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Event.thy Thu Sep 28 23:42:35 2006 +0200
@@ -27,11 +27,10 @@
text{*The constant "spies" is retained for compatibility's sake*}
-syntax
+
+abbreviation (input)
spies :: "event list => msg set"
-
-translations
- "spies" => "knows Spy"
+ "spies == knows Spy"
text{*Spy has access to his own key for spoof messages, but Server is secure*}
specification (bad)
--- a/src/HOL/Auth/Guard/Extensions.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy Thu Sep 28 23:42:35 2006 +0200
@@ -85,9 +85,9 @@
lemma Crypt_isnt_MPair [iff]: "~ is_MPair (Crypt K X)"
by simp
-syntax not_MPair :: "msg => bool"
-
-translations "not_MPair X" == "~ is_MPair X"
+abbreviation
+ not_MPair :: "msg => bool"
+ "not_MPair X == ~ is_MPair X"
lemma is_MPairE: "[| is_MPair X ==> P; not_MPair X ==> P |] ==> P"
by auto
@@ -369,11 +369,9 @@
| Notes A' X => if A=A' then insert X (knows' A evs) else knows' A evs
))"
-translations "spies" == "knows Spy"
-
-syntax spies' :: "event list => msg set"
-
-translations "spies'" == "knows' Spy"
+abbreviation
+ spies' :: "event list => msg set"
+ "spies' == knows' Spy"
subsubsection{*decomposition of knows into knows' and initState*}
@@ -453,9 +451,9 @@
constdefs knows_max :: "agent => event list => msg set"
"knows_max A evs == knows_max' A evs Un initState A"
-consts spies_max :: "event list => msg set"
-
-translations "spies_max evs" == "knows_max Spy evs"
+abbreviation
+ spies_max :: "event list => msg set"
+ "spies_max evs == knows_max Spy evs"
subsubsection{*basic facts about @{term knows_max}*}
--- a/src/HOL/Auth/Guard/Guard.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy Thu Sep 28 23:42:35 2006 +0200
@@ -162,9 +162,9 @@
subsection{*set obtained by decrypting a message*}
-syntax decrypt :: "msg set => key => msg => msg set"
-
-translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
+abbreviation (input)
+ decrypt :: "msg set => key => msg => msg set"
+ "decrypt H K Y == insert Y (H - {Crypt K Y})"
lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Nonce n:analz H |]
==> Nonce n:analz (decrypt H K Y)"
--- a/src/HOL/Auth/Guard/GuardK.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Thu Sep 28 23:42:35 2006 +0200
@@ -158,9 +158,9 @@
subsection{*set obtained by decrypting a message*}
-syntax decrypt :: "msg set => key => msg => msg set"
-
-translations "decrypt H K Y" => "insert Y (H - {Crypt K Y})"
+abbreviation (input)
+ decrypt :: "msg set => key => msg => msg set"
+ "decrypt H K Y == insert Y (H - {Crypt K Y})"
lemma analz_decrypt: "[| Crypt K Y:H; Key (invKey K):H; Key n:analz H |]
==> Key n:analz (decrypt H K Y)"
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Sep 28 23:42:35 2006 +0200
@@ -17,28 +17,22 @@
subsection{*messages used in the protocol*}
-syntax ns1 :: "agent => agent => nat => event"
-
-translations "ns1 A B NA" => "Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
+abbreviation (input)
+ ns1 :: "agent => agent => nat => event"
+ "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-syntax ns1' :: "agent => agent => agent => nat => event"
-
-translations "ns1' A' A B NA"
-=> "Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-
-syntax ns2 :: "agent => agent => nat => nat => event"
+ ns1' :: "agent => agent => agent => nat => event"
+ "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
-translations "ns2 B A NA NB"
-=> "Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-
-syntax ns2' :: "agent => agent => agent => nat => nat => event"
+ ns2 :: "agent => agent => nat => nat => event"
+ "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-translations "ns2' B' B A NA NB"
-=> "Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
+ ns2' :: "agent => agent => agent => nat => nat => event"
+ "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
-syntax ns3 :: "agent => agent => nat => event"
+ ns3 :: "agent => agent => nat => event"
+ "ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))"
-translations "ns3 A B NB" => "Says A B (Crypt (pubK B) (Nonce NB))"
subsection{*definition of the protocol*}
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Sep 28 23:42:35 2006 +0200
@@ -15,53 +15,42 @@
subsection{*messages used in the protocol*}
-syntax nil :: "msg"
-
-translations "nil" == "Number 0"
-
-syntax or1 :: "agent => agent => nat => event"
-
-translations "or1 A B NA"
-=> "Says A B {|Nonce NA, Agent A, Agent B,
- Ciph A {|Nonce NA, Agent A, Agent B|}|}"
+abbreviation
+ nil :: "msg"
+ "nil == Number 0"
-syntax or1' :: "agent => agent => agent => nat => msg => event"
-
-translations "or1' A' A B NA X"
-=> "Says A' B {|Nonce NA, Agent A, Agent B, X|}"
+ or1 :: "agent => agent => nat => event"
+ "or1 A B NA ==
+ Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
-syntax or2 :: "agent => agent => nat => nat => msg => event"
+ or1' :: "agent => agent => agent => nat => msg => event"
+ "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
-translations "or2 A B NA NB X"
-=> "Says B Server {|Nonce NA, Agent A, Agent B, X,
+ or2 :: "agent => agent => nat => nat => msg => event"
+ "or2 A B NA NB X ==
+ Says B Server {|Nonce NA, Agent A, Agent B, X,
Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
-syntax or2' :: "agent => agent => agent => nat => nat => event"
-
-translations "or2' B' A B NA NB"
-=> "Says B' Server {|Nonce NA, Agent A, Agent B,
+ or2' :: "agent => agent => agent => nat => nat => event"
+ "or2' B' A B NA NB ==
+ Says B' Server {|Nonce NA, Agent A, Agent B,
Ciph A {|Nonce NA, Agent A, Agent B|},
Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
-syntax or3 :: "agent => agent => nat => nat => key => event"
-
-translations "or3 A B NA NB K"
-=> "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
+ or3 :: "agent => agent => nat => nat => key => event"
+ "or3 A B NA NB K ==
+ Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
Ciph B {|Nonce NB, Key K|}|}"
-syntax or3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "or3' S Y A B NA NB K"
-=> "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
-
-syntax or4 :: "agent => agent => nat => msg => event"
+ or3':: "agent => msg => agent => agent => nat => nat => key => event"
+ "or3' S Y A B NA NB K ==
+ Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
-translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}"
+ or4 :: "agent => agent => nat => msg => event"
+ "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
-syntax or4' :: "agent => agent => nat => msg => event"
-
-translations "or4' B' A NA K" =>
-"Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
+ or4' :: "agent => agent => nat => key => event"
+ "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
subsection{*definition of the protocol*}
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Sep 28 23:42:35 2006 +0200
@@ -15,42 +15,34 @@
subsection{*messages used in the protocol*}
-syntax ya1 :: "agent => agent => nat => event"
-
-translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
+abbreviation (input)
+ ya1 :: "agent => agent => nat => event"
+ "ya1 A B NA == Says A B {|Agent A, Nonce NA|}"
-syntax ya1' :: "agent => agent => agent => nat => event"
-
-translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
-
-syntax ya2 :: "agent => agent => nat => nat => event"
+ ya1' :: "agent => agent => agent => nat => event"
+ "ya1' A' A B NA == Says A' B {|Agent A, Nonce NA|}"
-translations "ya2 A B NA NB"
-=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-
-syntax ya2' :: "agent => agent => agent => nat => nat => event"
+ ya2 :: "agent => agent => nat => nat => event"
+ "ya2 A B NA NB == Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-translations "ya2' B' A B NA NB"
-=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
+ ya2' :: "agent => agent => agent => nat => nat => event"
+ "ya2' B' A B NA NB == Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
-syntax ya3 :: "agent => agent => nat => nat => key => event"
-
-translations "ya3 A B NA NB K"
-=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
+ ya3 :: "agent => agent => nat => nat => key => event"
+ "ya3 A B NA NB K ==
+ Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
Ciph B {|Agent A, Key K|}|}"
-syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
-
-translations "ya3' S Y A B NA NB K"
-=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
+ ya3':: "agent => msg => agent => agent => nat => nat => key => event"
+ "ya3' S Y A B NA NB K ==
+ Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
-syntax ya4 :: "agent => agent => nat => nat => msg => event"
-
-translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
+ ya4 :: "agent => agent => nat => nat => msg => event"
+ "ya4 A B K NB Y == Says A B {|Y, Crypt K (Nonce NB)|}"
-syntax ya4' :: "agent => agent => nat => nat => msg => event"
+ ya4' :: "agent => agent => nat => nat => msg => event"
+ "ya4' A' B K NB Y == Says A' B {|Y, Crypt K (Nonce NB)|}"
-translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
subsection{*definition of the protocol*}
--- a/src/HOL/Auth/Guard/List_Msg.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/List_Msg.thy Thu Sep 28 23:42:35 2006 +0200
@@ -17,15 +17,15 @@
subsubsection{*nil is represented by any message which is not a pair*}
-syntax cons :: "msg => msg => msg"
-
-translations "cons x l" => "{|x,l|}"
+abbreviation (input)
+ cons :: "msg => msg => msg"
+ "cons x l == {|x,l|}"
subsubsection{*induction principle*}
lemma lmsg_induct: "[| !!x. not_MPair x ==> P x; !!x l. P l ==> P (cons x l) |]
==> P l"
-by (induct l, auto)
+by (induct l) auto
subsubsection{*head*}
@@ -50,7 +50,7 @@
"len other = 0"
lemma len_not_empty: "n < len l ==> EX x l'. l = cons x l'"
-by (cases l, auto)
+by (cases l) auto
subsubsection{*membership*}
@@ -69,10 +69,10 @@
"del (x, other) = other"
lemma notin_del [simp]: "~ isin (x,l) ==> del (x,l) = l"
-by (induct l, auto)
+by (induct l) auto
lemma isin_del [rule_format]: "isin (y, del (x,l)) --> isin (y,l)"
-by (induct l, auto)
+by (induct l) auto
subsubsection{*concatenation*}
@@ -83,7 +83,7 @@
"app (other, l') = l'"
lemma isin_app [iff]: "isin (x, app(l,l')) = (isin (x,l) | isin (x,l'))"
-by (induct l, auto)
+by (induct l) auto
subsubsection{*replacement*}
@@ -104,7 +104,7 @@
"ith (other, i) = other"
lemma ith_head: "0 < len l ==> ith (l,0) = head l"
-by (cases l, auto)
+by (cases l) auto
subsubsection{*insertion*}
@@ -115,7 +115,7 @@
"ins (l, 0, y) = cons y l"
lemma ins_head [simp]: "ins (l,0,y) = cons y l"
-by (cases l, auto)
+by (cases l) auto
subsubsection{*truncation*}
@@ -126,16 +126,16 @@
"trunc (cons x l, Suc i) = trunc (l,i)"
lemma trunc_zero [simp]: "trunc (l,0) = l"
-by (cases l, auto)
+by (cases l) auto
subsection{*Agent Lists*}
subsubsection{*set of well-formed agent-list messages*}
-syntax nil :: msg
-
-translations "nil" == "Number 0"
+abbreviation
+ nil :: msg
+ "nil == Number 0"
consts agl :: "msg set"
--- a/src/HOL/Auth/Guard/Proto.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Guard/Proto.thy Thu Sep 28 23:42:35 2006 +0200
@@ -17,9 +17,9 @@
types rule = "event set * event"
-syntax msg' :: "rule => msg"
-
-translations "msg' R" == "msg (snd R)"
+abbreviation
+ msg' :: "rule => msg"
+ "msg' R == msg (snd R)"
types proto = "rule set"
@@ -76,17 +76,18 @@
"ap s (Gets A X) = Gets (agent s A) (apm s X)"
"ap s (Notes A X) = Notes (agent s A) (apm s X)"
-syntax
-ap' :: "rule => msg"
-apm' :: "rule => msg"
-priK' :: "subs => agent => key"
-pubK' :: "subs => agent => key"
+abbreviation
+ ap' :: "subs => rule => event"
+ "ap' s R == ap s (snd R)"
-translations
-"ap' s R" == "ap s (snd R)"
-"apm' s R" == "apm s (msg' R)"
-"priK' s A" == "priK (agent s A)"
-"pubK' s A" == "pubK (agent s A)"
+ apm' :: "subs => rule => msg"
+ "apm' s R == apm s (msg' R)"
+
+ priK' :: "subs => agent => key"
+ "priK' s A == priK (agent s A)"
+
+ pubK' :: "subs => agent => key"
+ "pubK' s A == pubK (agent s A)"
subsection{*nonces generated by a rule*}
@@ -377,32 +378,31 @@
consts
ns :: proto
-ns1 :: rule
-ns2 :: rule
-ns3 :: rule
-translations
-"ns1" == "({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
+abbreviation
+ ns1 :: rule
+ "ns1 == ({}, Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}))"
-"ns2" == "({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
-Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
+ ns2 :: rule
+ "ns2 == ({Says a' b (Crypt (pubK b) {|Nonce Na, Agent a|})},
+ Says b a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|}))"
-"ns3" == "({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
-Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
-Says a b (Crypt (pubK b) (Nonce Nb)))"
+ ns3 :: rule
+ "ns3 == ({Says a b (Crypt (pubK b) {|Nonce Na, Agent a|}),
+ Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})},
+ Says a b (Crypt (pubK b) (Nonce Nb)))"
inductive ns intros
[iff]: "ns1:ns"
[iff]: "ns2:ns"
[iff]: "ns3:ns"
-syntax
-ns3a :: msg
-ns3b :: msg
+abbreviation (input)
+ ns3a :: event
+ "ns3a == Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
-translations
-"ns3a" => "Says a b (Crypt (pubK b) {|Nonce Na, Agent a|})"
-"ns3b" => "Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
+ ns3b :: event
+ "ns3b == Says b' a (Crypt (pubK a) {|Nonce Na, Nonce Nb, Agent b|})"
constdefs keys :: "keyfun"
"keys R' s' n evs == {priK' s' a, priK' s' b}"
--- a/src/HOL/Auth/KerberosIV.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Thu Sep 28 23:42:35 2006 +0200
@@ -10,33 +10,18 @@
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
-syntax
+abbreviation
Kas :: agent
- Tgs :: agent --{*the two servers are translations...*}
+ "Kas == Server"
-
-translations
- "Kas" == "Server "
- "Tgs" == "Friend 0"
+ Tgs :: agent
+ "Tgs == Friend 0"
axioms
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
-(*The current time is the length of the trace*)
-syntax
- CT :: "event list=>nat"
-
- expiredAK :: "[nat, event list] => bool"
-
- expiredSK :: "[nat, event list] => bool"
-
- expiredA :: "[nat, event list] => bool"
-
- valid :: "[nat, nat] => bool" ("valid _ wrt _")
-
-
constdefs
(* authKeys are those contained in an authTicket *)
authKeys :: "event list => key set"
@@ -92,16 +77,22 @@
replylife_LB [iff]: "Suc 0 \<le> replylife"
by blast
-translations
- "CT" == "length "
+abbreviation
+ (*The current time is the length of the trace*)
+ CT :: "event list=>nat"
+ "CT == length"
- "expiredAK Ta evs" == "authKlife + Ta < CT evs"
+ expiredAK :: "[nat, event list] => bool"
+ "expiredAK Ta evs == authKlife + Ta < CT evs"
- "expiredSK Ts evs" == "servKlife + Ts < CT evs"
+ expiredSK :: "[nat, event list] => bool"
+ "expiredSK Ts evs == servKlife + Ts < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
- "valid T1 wrt T2" == "T1 <= replylife + T2"
+ valid :: "[nat, nat] => bool" ("valid _ wrt _")
+ "valid T1 wrt T2 == T1 <= replylife + T2"
(*---------------------------------------------------------------------*)
--- a/src/HOL/Auth/KerberosIV_Gets.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Thu Sep 28 23:42:35 2006 +0200
@@ -10,33 +10,18 @@
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
-syntax
+abbreviation
Kas :: agent
- Tgs :: agent --{*the two servers are translations...*}
+ "Kas == Server"
-
-translations
- "Kas" == "Server "
- "Tgs" == "Friend 0"
+ Tgs :: agent
+ "Tgs == Friend 0"
axioms
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
-(*The current time is just the length of the trace!*)
-syntax
- CT :: "event list=>nat"
-
- expiredAK :: "[nat, event list] => bool"
-
- expiredSK :: "[nat, event list] => bool"
-
- expiredA :: "[nat, event list] => bool"
-
- valid :: "[nat, nat] => bool" ("valid _ wrt _")
-
-
constdefs
(* authKeys are those contained in an authTicket *)
authKeys :: "event list => key set"
@@ -80,16 +65,22 @@
replylife_LB [iff]: "Suc 0 \<le> replylife"
by blast
-translations
- "CT" == "length "
+abbreviation
+ (*The current time is just the length of the trace!*)
+ CT :: "event list=>nat"
+ "CT == length"
- "expiredAK Ta evs" == "authKlife + Ta < CT evs"
+ expiredAK :: "[nat, event list] => bool"
+ "expiredAK Ta evs == authKlife + Ta < CT evs"
- "expiredSK Ts evs" == "servKlife + Ts < CT evs"
+ expiredSK :: "[nat, event list] => bool"
+ "expiredSK Ts evs == servKlife + Ts < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
- "valid T1 wrt T2" == "T1 <= replylife + T2"
+ valid :: "[nat, nat] => bool" ("valid _ wrt _")
+ "valid T1 wrt T2 == T1 <= replylife + T2"
(*---------------------------------------------------------------------*)
--- a/src/HOL/Auth/KerberosV.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/KerberosV.thy Thu Sep 28 23:42:35 2006 +0200
@@ -8,33 +8,18 @@
text{*The "u" prefix indicates theorems referring to an updated version of the protocol. The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*}
-syntax
+abbreviation
Kas :: agent
- Tgs :: agent --{*the two servers are translations...*}
+ "Kas == Server"
-
-translations
- "Kas" == "Server "
- "Tgs" == "Friend 0"
+ Tgs :: agent
+ "Tgs == Friend 0"
axioms
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
-(*The current time is just the length of the trace!*)
-syntax
- CT :: "event list=>nat"
-
- expiredAK :: "[nat, event list] => bool"
-
- expiredSK :: "[nat, event list] => bool"
-
- expiredA :: "[nat, event list] => bool"
-
- valid :: "[nat, nat] => bool" ("valid _ wrt _")
-
-
constdefs
(* authKeys are those contained in an authTicket *)
authKeys :: "event list => key set"
@@ -81,16 +66,22 @@
replylife_LB [iff]: "Suc 0 \<le> replylife"
by blast
-translations
- "CT" == "length "
+abbreviation
+ (*The current time is just the length of the trace!*)
+ CT :: "event list=>nat"
+ "CT == length"
- "expiredAK T evs" == "authKlife + T < CT evs"
+ expiredAK :: "[nat, event list] => bool"
+ "expiredAK T evs == authKlife + T < CT evs"
- "expiredSK T evs" == "servKlife + T < CT evs"
+ expiredSK :: "[nat, event list] => bool"
+ "expiredSK T evs == servKlife + T < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
- "valid T1 wrt T2" == "T1 <= replylife + T2"
+ valid :: "[nat, nat] => bool" ("valid _ wrt _")
+ "valid T1 wrt T2 == T1 <= replylife + T2"
(*---------------------------------------------------------------------*)
--- a/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Thu Sep 28 23:42:35 2006 +0200
@@ -20,11 +20,6 @@
(* Temporal model of accidents: session keys can be leaked
ONLY when they have expired *)
-syntax
- CT :: "event list=>nat"
- expiredK :: "[nat, event list] => bool"
- expiredA :: "[nat, event list] => bool"
-
consts
(*Duration of the session key*)
@@ -43,13 +38,15 @@
authlife_LB [iff]: "0 < authlife"
by blast
-
-translations
- "CT" == "length "
+abbreviation
+ CT :: "event list=>nat"
+ "CT == length "
- "expiredK T evs" == "sesKlife + T < CT evs"
+ expiredK :: "[nat, event list] => bool"
+ "expiredK T evs == sesKlife + T < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
constdefs
--- a/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Kerberos_BAN_Gets.thy Thu Sep 28 23:42:35 2006 +0200
@@ -18,11 +18,6 @@
(* Temporal modelization: session keys can be leaked
ONLY when they have expired *)
-syntax
- CT :: "event list=>nat"
- expiredK :: "[nat, event list] => bool"
- expiredA :: "[nat, event list] => bool"
-
consts
(*Duration of the session key*)
@@ -44,12 +39,15 @@
by blast
-translations
- "CT" == "length "
+abbreviation
+ CT :: "event list=>nat"
+ "CT == length"
- "expiredK T evs" == "sesKlife + T < CT evs"
+ expiredK :: "[nat, event list] => bool"
+ "expiredK T evs == sesKlife + T < CT evs"
- "expiredA T evs" == "authlife + T < CT evs"
+ expiredA :: "[nat, event list] => bool"
+ "expiredA T evs == authlife + T < CT evs"
constdefs
--- a/src/HOL/Auth/Public.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Public.thy Thu Sep 28 23:42:35 2006 +0200
@@ -20,33 +20,32 @@
consts
publicKey :: "[keymode,agent] => key"
-syntax
+abbreviation
pubEK :: "agent => key"
- pubSK :: "agent => key"
+ "pubEK == publicKey Encryption"
- privateKey :: "[bool,agent] => key"
- priEK :: "agent => key"
- priSK :: "agent => key"
+ pubSK :: "agent => key"
+ "pubSK == publicKey Signature"
-translations
- "pubEK" == "publicKey Encryption"
- "pubSK" == "publicKey Signature"
+ privateKey :: "[keymode, agent] => key"
+ "privateKey b A == invKey (publicKey b A)"
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*)
- "privateKey b A" == "invKey (publicKey b A)"
- "priEK A" == "privateKey Encryption A"
- "priSK A" == "privateKey Signature A"
+ priEK :: "agent => key"
+ "priEK A == privateKey Encryption A"
+ priSK :: "agent => key"
+ "priSK A == privateKey Signature A"
-text{*These translations give backward compatibility. They represent the
+text{*These abbreviations give backward compatibility. They represent the
simple situation where the signature and encryption keys are the same.*}
-syntax
+
+abbreviation
pubK :: "agent => key"
+ "pubK A == pubEK A"
+
priK :: "agent => key"
-
-translations
- "pubK A" == "pubEK A"
- "priK A" == "invKey (pubEK A)"
+ "priK A == invKey (pubEK A)"
text{*By freeness of agents, no two agents have the same key. Since
--- a/src/HOL/Auth/Recur.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Recur.thy Thu Sep 28 23:42:35 2006 +0200
@@ -9,8 +9,9 @@
theory Recur imports Public begin
text{*End marker for message bundles*}
-syntax END :: "msg"
-translations "END" == "Number 0"
+abbreviation
+ END :: "msg"
+ "END == Number 0"
(*Two session keys are distributed to each agent except for the initiator,
who receives one.
--- a/src/HOL/Auth/Smartcard/EventSC.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Thu Sep 28 23:42:35 2006 +0200
@@ -24,10 +24,9 @@
cloned :: "card set" (* cloned smart cards*)
secureM :: "bool"(*assumption of secure means between agents and their cards*)
-syntax
+abbreviation
insecureM :: bool (*certain protocols make no assumption of secure means*)
-translations
- "insecureM" == "\<not>secureM"
+ "insecureM == \<not>secureM"
text{*Spy has access to his own key for spoof messages, but Server is secure*}
--- a/src/HOL/Auth/TLS.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/TLS.thy Thu Sep 28 23:42:35 2006 +0200
@@ -63,13 +63,13 @@
Session keys implicitly include MAC secrets.*)
sessionK :: "(nat*nat*nat) * role => key"
-syntax
- clientK :: "nat*nat*nat => key"
- serverK :: "nat*nat*nat => key"
+abbreviation
+ clientK :: "nat*nat*nat => key"
+ "clientK X == sessionK(X, ClientRole)"
-translations
- "clientK X" == "sessionK(X, ClientRole)"
- "serverK X" == "sessionK(X, ServerRole)"
+ serverK :: "nat*nat*nat => key"
+ "serverK X == sessionK(X, ServerRole)"
+
specification (PRF)
inj_PRF: "inj PRF"
--- a/src/HOL/Auth/ZhouGollmann.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy Thu Sep 28 23:42:35 2006 +0200
@@ -12,23 +12,18 @@
theory ZhouGollmann imports Public begin
-syntax
+abbreviation
TTP :: agent
+ "TTP == Server"
-translations
- "TTP" == " Server "
-
-syntax
f_sub :: nat
+ "f_sub == 5"
f_nro :: nat
+ "f_nro == 2"
f_nrr :: nat
+ "f_nrr == 3"
f_con :: nat
-
-translations
- "f_sub" == " 5 "
- "f_nro" == " 2 "
- "f_nrr" == " 3 "
- "f_con" == " 4 "
+ "f_con == 4"
constdefs
--- a/src/HOL/MicroJava/J/Example.thy Thu Sep 28 23:42:32 2006 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Thu Sep 28 23:42:35 2006 +0200
@@ -110,28 +110,20 @@
Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
-syntax
+abbreviation
+ NP :: xcpt
+ "NP == NullPointer"
- NP :: xcpt
tprg ::"java_mb prog"
+ "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
+
obj1 :: obj
- obj2 :: obj
- s0 :: state
- s1 :: state
- s2 :: state
- s3 :: state
- s4 :: state
+ "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
-translations
- "NP" == "NullPointer"
- "tprg" == "[ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
- "obj1" <= "(Ext, empty((vee, Base)\<mapsto>Bool False)
- ((vee, Ext )\<mapsto>Intg 0))"
- "s0" == " Norm (empty, empty)"
- "s1" == " Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
- "s2" == " Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
- "s3" == "(Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
-
+ "s0 == Norm (empty, empty)"
+ "s1 == Norm (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
+ "s2 == Norm (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
+ "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
ML {* bind_thm ("map_of_Cons", hd (tl (thms "map_of.simps"))) *}
lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"