src/HOL/Auth/Recur.thy
changeset 23746 a455e69c31cc
parent 21404 eb85850d3eb7
child 23894 1a4167d761ac
     1.1 --- a/src/HOL/Auth/Recur.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/Auth/Recur.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -17,16 +17,17 @@
     1.4          who receives one.
     1.5    Perhaps the two session keys could be bundled into a single message.
     1.6  *)
     1.7 -consts     respond :: "event list => (msg*msg*key)set"
     1.8 -inductive "respond evs" (*Server's response to the nested message*)
     1.9 -  intros
    1.10 +inductive_set (*Server's response to the nested message*)
    1.11 +  respond :: "event list => (msg*msg*key)set"
    1.12 +  for evs :: "event list"
    1.13 +  where
    1.14     One:  "Key KAB \<notin> used evs
    1.15            ==> (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|},
    1.16                 {|Crypt (shrK A) {|Key KAB, Agent B, Nonce NA|}, END|},
    1.17                 KAB)   \<in> respond evs"
    1.18  
    1.19      (*The most recent session key is passed up to the caller*)
    1.20 -   Cons: "[| (PA, RA, KAB) \<in> respond evs;
    1.21 + | Cons: "[| (PA, RA, KAB) \<in> respond evs;
    1.22               Key KBC \<notin> used evs;  Key KBC \<notin> parts {RA};
    1.23               PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} |]
    1.24            ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|},
    1.25 @@ -40,50 +41,50 @@
    1.26  (*Induction over "respond" can be difficult due to the complexity of the
    1.27    subgoals.  Set "responses" captures the general form of certificates.
    1.28  *)
    1.29 -consts     responses :: "event list => msg set"
    1.30 -inductive "responses evs"
    1.31 -  intros
    1.32 +inductive_set
    1.33 +  responses :: "event list => msg set"
    1.34 +  for evs :: "event list"
    1.35 +  where
    1.36      (*Server terminates lists*)
    1.37     Nil:  "END \<in> responses evs"
    1.38  
    1.39 -   Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
    1.40 + | Cons: "[| RA \<in> responses evs;  Key KAB \<notin> used evs |]
    1.41            ==> {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|},
    1.42                  RA|}  \<in> responses evs"
    1.43  
    1.44  
    1.45 -consts     recur   :: "event list set"
    1.46 -inductive "recur"
    1.47 -  intros
    1.48 +inductive_set recur :: "event list set"
    1.49 +  where
    1.50           (*Initial trace is empty*)
    1.51     Nil:  "[] \<in> recur"
    1.52  
    1.53           (*The spy MAY say anything he CAN say.  Common to
    1.54             all similar protocols.*)
    1.55 -   Fake: "[| evsf \<in> recur;  X \<in> synth (analz (knows Spy evsf)) |]
    1.56 + | Fake: "[| evsf \<in> recur;  X \<in> synth (analz (knows Spy evsf)) |]
    1.57            ==> Says Spy B X  # evsf \<in> recur"
    1.58  
    1.59           (*Alice initiates a protocol run.
    1.60             END is a placeholder to terminate the nesting.*)
    1.61 -   RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
    1.62 + | RA1:  "[| evs1 \<in> recur;  Nonce NA \<notin> used evs1 |]
    1.63            ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, END|})
    1.64                # evs1 \<in> recur"
    1.65  
    1.66           (*Bob's response to Alice's message.  C might be the Server.
    1.67             We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because
    1.68             it complicates proofs, so B may respond to any message at all!*)
    1.69 -   RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
    1.70 + | RA2:  "[| evs2 \<in> recur;  Nonce NB \<notin> used evs2;
    1.71               Says A' B PA \<in> set evs2 |]
    1.72            ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|})
    1.73                # evs2 \<in> recur"
    1.74  
    1.75           (*The Server receives Bob's message and prepares a response.*)
    1.76 -   RA3:  "[| evs3 \<in> recur;  Says B' Server PB \<in> set evs3;
    1.77 + | RA3:  "[| evs3 \<in> recur;  Says B' Server PB \<in> set evs3;
    1.78               (PB,RB,K) \<in> respond evs3 |]
    1.79            ==> Says Server B RB # evs3 \<in> recur"
    1.80  
    1.81           (*Bob receives the returned message and compares the Nonces with
    1.82             those in the message he previously sent the Server.*)
    1.83 -   RA4:  "[| evs4 \<in> recur;
    1.84 + | RA4:  "[| evs4 \<in> recur;
    1.85               Says B  C {|XH, Agent B, Agent C, Nonce NB,
    1.86                           XA, Agent A, Agent B, Nonce NA, P|} \<in> set evs4;
    1.87               Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|},
    1.88 @@ -350,7 +351,7 @@
    1.89  lemma respond_certificate:
    1.90       "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \<in> respond evs
    1.91        ==> Crypt (shrK A) {|Key K, B, NA|} \<in> parts {RA}"
    1.92 -apply (ind_cases "(X, RA, K) \<in> respond evs")
    1.93 +apply (ind_cases "(Hash[Key (shrK A)] \<lbrace>Agent A, B, NA, P\<rbrace>, RA, K) \<in> respond evs")
    1.94  apply simp_all
    1.95  done
    1.96