--- a/src/HOL/Auth/Yahalom2.thy Wed Jul 11 11:13:08 2007 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Wed Jul 11 11:14:51 2007 +0200
@@ -19,29 +19,28 @@
This theory has the prototypical example of a secrecy relation, KeyCryptNonce.
*}
-consts yahalom :: "event list set"
-inductive "yahalom"
- intros
+inductive_set yahalom :: "event list set"
+ where
(*Initial trace is empty*)
Nil: "[] \<in> yahalom"
(*The spy MAY say anything he CAN say. We do not expect him to
invent new nonces here, but he can also use NS1. Common to
all similar protocols.*)
- Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |]
+ | Fake: "[| evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) |]
==> Says Spy B X # evsf \<in> yahalom"
(*A message that has been sent can be received by the
intended recipient.*)
- Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |]
+ | Reception: "[| evsr \<in> yahalom; Says A B X \<in> set evsr |]
==> Gets B X # evsr \<in> yahalom"
(*Alice initiates a protocol run*)
- YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
+ | YM1: "[| evs1 \<in> yahalom; Nonce NA \<notin> used evs1 |]
==> Says A B {|Agent A, Nonce NA|} # evs1 \<in> yahalom"
(*Bob's response to Alice's message.*)
- YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
+ | YM2: "[| evs2 \<in> yahalom; Nonce NB \<notin> used evs2;
Gets B {|Agent A, Nonce NA|} \<in> set evs2 |]
==> Says B Server
{|Agent B, Nonce NB, Crypt (shrK B) {|Agent A, Nonce NA|}|}
@@ -50,7 +49,7 @@
(*The Server receives Bob's message. He responds by sending a
new session key to Alice, with a certificate for forwarding to Bob.
Both agents are quoted in the 2nd certificate to prevent attacks!*)
- YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
+ | YM3: "[| evs3 \<in> yahalom; Key KAB \<notin> used evs3;
Gets Server {|Agent B, Nonce NB,
Crypt (shrK B) {|Agent A, Nonce NA|}|}
\<in> set evs3 |]
@@ -62,7 +61,7 @@
(*Alice receives the Server's (?) message, checks her Nonce, and
uses the new session key to send Bob his Nonce.*)
- YM4: "[| evs4 \<in> yahalom;
+ | YM4: "[| evs4 \<in> yahalom;
Gets A {|Nonce NB, Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} \<in> set evs4;
Says A B {|Agent A, Nonce NA|} \<in> set evs4 |]
@@ -71,7 +70,7 @@
(*This message models possible leaks of session keys. The nonces
identify the protocol run. Quoting Server here ensures they are
correct. *)
- Oops: "[| evso \<in> yahalom;
+ | Oops: "[| evso \<in> yahalom;
Says Server A {|Nonce NB,
Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
X|} \<in> set evso |]