src/HOL/Auth/NS_Shared.thy
changeset 23746 a455e69c31cc
parent 18886 9f27383426db
child 32404 da3ca3c6ec81
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -25,26 +25,25 @@
     1.4        X \<notin> parts (spies (takeWhile (% z. z  \<noteq> Says A B Y) (rev evs)))"
     1.5  
     1.6  
     1.7 -consts  ns_shared   :: "event list set"
     1.8 -inductive "ns_shared"
     1.9 - intros
    1.10 +inductive_set ns_shared :: "event list set"
    1.11 + where
    1.12  	(*Initial trace is empty*)
    1.13    Nil:  "[] \<in> ns_shared"
    1.14  	(*The spy MAY say anything he CAN say.  We do not expect him to
    1.15  	  invent new nonces here, but he can also use NS1.  Common to
    1.16  	  all similar protocols.*)
    1.17 -  Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    1.18 +| Fake: "\<lbrakk>evsf \<in> ns_shared;  X \<in> synth (analz (spies evsf))\<rbrakk>
    1.19  	 \<Longrightarrow> Says Spy B X # evsf \<in> ns_shared"
    1.20  
    1.21  	(*Alice initiates a protocol run, requesting to talk to any B*)
    1.22 -  NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    1.23 +| NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    1.24  	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    1.25  
    1.26  	(*Server's response to Alice's message.
    1.27  	  !! It may respond more than once to A's request !!
    1.28  	  Server doesn't know who the true sender is, hence the A' in
    1.29  	      the sender field.*)
    1.30 -  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    1.31 +| NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    1.32  	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    1.33  	 \<Longrightarrow> Says Server A
    1.34  	       (Crypt (shrK A)
    1.35 @@ -54,14 +53,14 @@
    1.36  
    1.37  	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.38  	   Need A \<noteq> Server because we allow messages to self.*)
    1.39 -  NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    1.40 +| NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    1.41  	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    1.42  	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    1.43  	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    1.44  
    1.45  	(*Bob's nonce exchange.  He does not know who the message came
    1.46  	  from, but responds to A because she is mentioned inside.*)
    1.47 -  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
    1.48 +| NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
    1.49  	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    1.50  	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    1.51  
    1.52 @@ -70,7 +69,7 @@
    1.53  	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.54  	  Letting the Spy add or subtract 1 lets him send all nonces.
    1.55  	  Instead we distinguish the messages by sending the nonce twice.*)
    1.56 -  NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
    1.57 +| NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
    1.58  	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.59  	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.60  	    \<in> set evs5\<rbrakk>
    1.61 @@ -79,7 +78,7 @@
    1.62  	(*This message models possible leaks of session keys.
    1.63  	  The two Nonces identify the protocol run: the rule insists upon
    1.64  	  the true senders in order to make them accurate.*)
    1.65 -  Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    1.66 +| Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    1.67  	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.68  	      \<in> set evso\<rbrakk>
    1.69  	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"