src/HOL/Auth/Smartcard/ShoupRubinBella.thy
author huffman
Sat Jun 06 09:11:12 2009 -0700 (2009-06-06)
changeset 31488 5691ccb8d6b5
parent 30549 d2d7874648bd
child 32149 ef59550a55d3
permissions -rw-r--r--
generalize tendsto to class topological_space
paulson@18886
     1
(*  ID:         $Id$
paulson@18886
     2
    Author:     Giampaolo Bella, Catania University
paulson@18886
     3
*)
paulson@18886
     4
paulson@18886
     5
header{*Bella's modification of the Shoup-Rubin protocol*}
paulson@18886
     6
paulson@18886
     7
theory ShoupRubinBella imports Smartcard begin
paulson@18886
     8
paulson@18886
     9
text{*The modifications are that message 7 now mentions A, while message 10
paulson@18886
    10
now mentions Nb and B. The lack of explicitness of the original version was
paulson@18886
    11
discovered by investigating adherence to the principle of Goal
paulson@18886
    12
Availability. Only the updated version makes the goals of confidentiality,
paulson@18886
    13
authentication and key distribution available to both peers.*}
paulson@18886
    14
paulson@18886
    15
consts
paulson@18886
    16
paulson@18886
    17
    sesK :: "nat*key => key"
paulson@18886
    18
paulson@18886
    19
axioms
paulson@18886
    20
     
paulson@18886
    21
   (*sesK is injective on each component*) 
paulson@18886
    22
   inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
paulson@18886
    23
paulson@18886
    24
   (*all long-term keys differ from sesK*)
paulson@18886
    25
   shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
paulson@18886
    26
   crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
paulson@18886
    27
   pin_disj_sesK  [iff]: "pin P \<noteq> sesK(m,pk)"
paulson@18886
    28
   pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
paulson@18886
    29
paulson@18886
    30
   (*needed for base case in analz_image_freshK*)
paulson@18886
    31
   Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
paulson@18886
    32
                   Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" 
paulson@18886
    33
paulson@18886
    34
  (*this protocol makes the assumption of secure means
paulson@18886
    35
    between each agent and his smartcard*)
paulson@18886
    36
   shouprubin_assumes_securemeans [iff]: "evs \<in> srb \<Longrightarrow> secureM"
paulson@18886
    37
paulson@18886
    38
constdefs
paulson@18886
    39
paulson@18886
    40
  Unique :: "[event, event list] => bool" ("Unique _ on _")
paulson@18886
    41
   "Unique ev on evs == 
paulson@18886
    42
      ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs))"
paulson@18886
    43
paulson@18886
    44
berghofe@23746
    45
inductive_set srb :: "event list set"
berghofe@23746
    46
  where
paulson@18886
    47
paulson@18886
    48
    Nil:  "[]\<in> srb"
paulson@18886
    49
paulson@18886
    50
paulson@18886
    51
berghofe@23746
    52
  | Fake: "\<lbrakk> evsF \<in> srb;  X \<in> synth (analz (knows Spy evsF)); 
paulson@18886
    53
             illegalUse(Card B) \<rbrakk>
paulson@18886
    54
          \<Longrightarrow> Says Spy A X # 
paulson@18886
    55
              Inputs Spy (Card B) X # evsF \<in> srb"
paulson@18886
    56
paulson@18886
    57
(*In general this rule causes the assumption Card B \<notin> cloned
paulson@18886
    58
  in most guarantees for B - starting with confidentiality -
paulson@18886
    59
  otherwise pairK_confidential could not apply*)
berghofe@23746
    60
  | Forge:
paulson@18886
    61
         "\<lbrakk> evsFo \<in> srb; Nonce Nb \<in> analz (knows Spy evsFo);
paulson@18886
    62
             Key (pairK(A,B)) \<in> knows Spy evsFo \<rbrakk>
paulson@18886
    63
          \<Longrightarrow> Notes Spy (Key (sesK(Nb,pairK(A,B)))) # evsFo \<in> srb"
paulson@18886
    64
paulson@18886
    65
paulson@18886
    66
berghofe@23746
    67
  | Reception: "\<lbrakk> evsrb\<in> srb; Says A B X \<in> set evsrb \<rbrakk>
paulson@18886
    68
              \<Longrightarrow> Gets B X # evsrb \<in> srb"
paulson@18886
    69
paulson@18886
    70
paulson@18886
    71
paulson@18886
    72
(*A AND THE SERVER*)
berghofe@23746
    73
  | SR_U1:  "\<lbrakk> evs1 \<in> srb; A \<noteq> Server \<rbrakk>
paulson@18886
    74
          \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> 
paulson@18886
    75
                # evs1 \<in> srb"
paulson@18886
    76
berghofe@23746
    77
  | SR_U2:  "\<lbrakk> evs2 \<in> srb; 
paulson@18886
    78
             Gets Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk>
paulson@18886
    79
          \<Longrightarrow> Says Server A \<lbrace>Nonce (Pairkey(A,B)), 
paulson@18886
    80
                           Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>
paulson@18886
    81
                  \<rbrace>
paulson@18886
    82
                # evs2 \<in> srb"
paulson@18886
    83
paulson@18886
    84
paulson@18886
    85
paulson@18886
    86
paulson@18886
    87
(*A AND HER CARD*)
paulson@18886
    88
(*A cannot decrypt the verifier for she dosn't know shrK A,
paulson@18886
    89
  but the pairkey is recognisable*)
berghofe@23746
    90
  | SR_U3:  "\<lbrakk> evs3 \<in> srb; legalUse(Card A);
paulson@18886
    91
             Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3;
paulson@18886
    92
             Gets A \<lbrace>Nonce Pk, Certificate\<rbrace> \<in> set evs3 \<rbrakk>
paulson@18886
    93
          \<Longrightarrow> Inputs A (Card A) (Agent A)
paulson@18886
    94
                # evs3 \<in> srb"   (*however A only queries her card 
paulson@18886
    95
if she has previously contacted the server to initiate with some B. 
paulson@18886
    96
Otherwise she would do so even if the Server had not been active. 
paulson@18886
    97
Still, this doesn't and can't mean that the pairkey originated with 
paulson@18886
    98
the server*)
paulson@18886
    99
 
paulson@18886
   100
(*The card outputs the nonce Na to A*)               
berghofe@23746
   101
  | SR_U4:  "\<lbrakk> evs4 \<in> srb; 
paulson@18886
   102
             Nonce Na \<notin> used evs4; legalUse(Card A); A \<noteq> Server;
paulson@18886
   103
             Inputs A (Card A) (Agent A) \<in> set evs4 \<rbrakk> 
paulson@18886
   104
       \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
paulson@18886
   105
              # evs4 \<in> srb"
paulson@18886
   106
paulson@18886
   107
(*The card can be exploited by the spy*)
paulson@18886
   108
(*because of the assumptions on the card, A is certainly not server nor spy*)
berghofe@23746
   109
  | SR_U4Fake: "\<lbrakk> evs4F \<in> srb; Nonce Na \<notin> used evs4F; 
paulson@18886
   110
             illegalUse(Card A);
paulson@18886
   111
             Inputs Spy (Card A) (Agent A) \<in> set evs4F \<rbrakk> 
paulson@18886
   112
      \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
paulson@18886
   113
            # evs4F \<in> srb"
paulson@18886
   114
paulson@18886
   115
paulson@18886
   116
paulson@18886
   117
paulson@18886
   118
(*A TOWARDS B*)
berghofe@23746
   119
  | SR_U5:  "\<lbrakk> evs5 \<in> srb; 
paulson@18886
   120
             Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs5;
paulson@18886
   121
             \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
paulson@18886
   122
          \<Longrightarrow> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> # evs5 \<in> srb"
paulson@18886
   123
(*A must check that the verifier is not a compound message, 
paulson@18886
   124
  otherwise this would also fire after SR_U7 *)
paulson@18886
   125
paulson@18886
   126
paulson@18886
   127
paulson@18886
   128
paulson@18886
   129
(*B AND HIS CARD*)
berghofe@23746
   130
  | SR_U6:  "\<lbrakk> evs6 \<in> srb; legalUse(Card B);
paulson@18886
   131
             Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs6 \<rbrakk>
paulson@18886
   132
          \<Longrightarrow> Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> 
paulson@18886
   133
                # evs6 \<in> srb"
paulson@18886
   134
(*B gets back from the card the session key and various verifiers*)
berghofe@23746
   135
  | SR_U7:  "\<lbrakk> evs7 \<in> srb; 
paulson@18886
   136
             Nonce Nb \<notin> used evs7; legalUse(Card B); B \<noteq> Server;
paulson@18886
   137
             K = sesK(Nb,pairK(A,B));
paulson@18886
   138
             Key K \<notin> used evs7;
paulson@18886
   139
             Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7\<rbrakk>
paulson@18886
   140
    \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,
paulson@18886
   141
                            Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   142
                            Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> 
paulson@18886
   143
                # evs7 \<in> srb"
paulson@18886
   144
(*The card can be exploited by the spy*)
paulson@18886
   145
(*because of the assumptions on the card, A is certainly not server nor spy*)
berghofe@23746
   146
  | SR_U7Fake:  "\<lbrakk> evs7F \<in> srb; Nonce Nb \<notin> used evs7F; 
paulson@18886
   147
             illegalUse(Card B);
paulson@18886
   148
             K = sesK(Nb,pairK(A,B));
paulson@18886
   149
             Key K \<notin> used evs7F;
paulson@18886
   150
             Inputs Spy (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs7F \<rbrakk>
paulson@18886
   151
          \<Longrightarrow> Outpts (Card B) Spy \<lbrace>Nonce Nb, Agent A, Key K,
paulson@18886
   152
                            Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   153
                            Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> 
paulson@18886
   154
                # evs7F \<in> srb"
paulson@18886
   155
paulson@18886
   156
paulson@18886
   157
paulson@18886
   158
paulson@18886
   159
(*B TOWARDS A*)
paulson@18886
   160
(*having sent an input that mentions A is the only memory B relies on,
paulson@18886
   161
  since the output doesn't mention A - lack of explicitness*) 
berghofe@23746
   162
  | SR_U8:  "\<lbrakk> evs8 \<in> srb;  
paulson@18886
   163
             Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs8;
paulson@18886
   164
             Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, 
paulson@18886
   165
                                 Cert1, Cert2\<rbrace> \<in> set evs8 \<rbrakk>
paulson@18886
   166
          \<Longrightarrow> Says B A \<lbrace>Nonce Nb, Cert1\<rbrace> # evs8 \<in> srb"
paulson@18886
   167
  
paulson@18886
   168
paulson@18886
   169
paulson@18886
   170
paulson@18886
   171
(*A AND HER CARD*)
paulson@18886
   172
(*A cannot check the form of the verifiers - although I can prove the form of
paulson@18886
   173
  Cert2 - and just feeds her card with what she's got*)
berghofe@23746
   174
  | SR_U9:  "\<lbrakk> evs9 \<in> srb; legalUse(Card A);
paulson@18886
   175
             Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs9;
paulson@18886
   176
             Outpts (Card A) A \<lbrace>Nonce Na, Cert2\<rbrace> \<in> set evs9; 
paulson@18886
   177
             Gets A \<lbrace>Nonce Nb, Cert3\<rbrace> \<in> set evs9;
paulson@18886
   178
             \<forall> p q. Cert2 \<noteq> \<lbrace>p, q\<rbrace> \<rbrakk>
paulson@18886
   179
          \<Longrightarrow> Inputs A (Card A) 
paulson@18886
   180
                 \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,
paulson@18886
   181
                  Cert1, Cert3, Cert2\<rbrace> 
paulson@18886
   182
                # evs9 \<in> srb"
paulson@18886
   183
(*But the card will only give outputs to the inputs of the correct form*)
berghofe@23746
   184
  | SR_U10: "\<lbrakk> evs10 \<in> srb; legalUse(Card A); A \<noteq> Server;
paulson@18886
   185
             K = sesK(Nb,pairK(A,B));
paulson@18886
   186
             Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, 
paulson@18886
   187
                                 Nonce (Pairkey(A,B)),
paulson@18886
   188
                                 Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), 
paulson@18886
   189
                                                   Agent B\<rbrace>,
paulson@18886
   190
                                 Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   191
                                 Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
paulson@18886
   192
               \<in> set evs10 \<rbrakk>
paulson@18886
   193
          \<Longrightarrow> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
paulson@18886
   194
                                 Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
paulson@18886
   195
                 # evs10 \<in> srb"
paulson@18886
   196
(*The card can be exploited by the spy*)
paulson@18886
   197
(*because of the assumptions on the card, A is certainly not server nor spy*)
berghofe@23746
   198
  | SR_U10Fake: "\<lbrakk> evs10F \<in> srb; 
paulson@18886
   199
             illegalUse(Card A);
paulson@18886
   200
             K = sesK(Nb,pairK(A,B));
paulson@18886
   201
             Inputs Spy (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, 
paulson@18886
   202
                                   Nonce (Pairkey(A,B)),
paulson@18886
   203
                                   Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), 
paulson@18886
   204
                                                    Agent B\<rbrace>,
paulson@18886
   205
                                   Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   206
                                   Crypt (crdK (Card A)) (Nonce Na)\<rbrace>
paulson@18886
   207
               \<in> set evs10F \<rbrakk>
paulson@18886
   208
          \<Longrightarrow> Outpts (Card A) Spy \<lbrace>Agent B, Nonce Nb, 
paulson@18886
   209
                                   Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>
paulson@18886
   210
                 # evs10F \<in> srb"
paulson@18886
   211
paulson@18886
   212
paulson@18886
   213
paulson@18886
   214
paulson@18886
   215
(*A TOWARDS B*)
paulson@18886
   216
(*having initiated with B is the only memory A relies on,
paulson@18886
   217
  since the output doesn't mention B - lack of explicitness*) 
berghofe@23746
   218
  | SR_U11: "\<lbrakk> evs11 \<in> srb;
paulson@18886
   219
             Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs11;
paulson@18886
   220
             Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
paulson@18886
   221
               \<in> set evs11 \<rbrakk>
paulson@18886
   222
          \<Longrightarrow> Says A B (Certificate) 
paulson@18886
   223
                 # evs11 \<in> srb"
paulson@18886
   224
paulson@18886
   225
paulson@18886
   226
paulson@18886
   227
(*Both peers may leak by accident the session keys obtained from their
paulson@18886
   228
  cards*)
berghofe@23746
   229
  | Oops1:
paulson@18886
   230
     "\<lbrakk> evsO1 \<in> srb;
paulson@18886
   231
         Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
paulson@18886
   232
           \<in> set evsO1 \<rbrakk>
paulson@18886
   233
     \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO1 \<in> srb"
paulson@18886
   234
berghofe@23746
   235
  | Oops2:
paulson@18886
   236
     "\<lbrakk> evsO2 \<in> srb;
paulson@18886
   237
         Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
paulson@18886
   238
           \<in> set evsO2 \<rbrakk>
paulson@18886
   239
    \<Longrightarrow> Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> # evsO2 \<in> srb"
paulson@18886
   240
paulson@18886
   241
paulson@18886
   242
paulson@18886
   243
paulson@18886
   244
paulson@18886
   245
paulson@18886
   246
(*To solve Fake case when it doesn't involve analz - used to be condensed
paulson@18886
   247
  into Fake_parts_insert_tac*)
paulson@18886
   248
declare Fake_parts_insert_in_Un  [dest]
paulson@18886
   249
declare analz_into_parts [dest]
paulson@18886
   250
(*declare parts_insertI [intro]*)
paulson@18886
   251
paulson@18886
   252
paulson@18886
   253
paulson@18886
   254
(*General facts about message reception*)
paulson@18886
   255
lemma Gets_imp_Says: 
paulson@18886
   256
       "\<lbrakk> Gets B X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> \<exists> A. Says A B X \<in> set evs"
paulson@18886
   257
apply (erule rev_mp, erule srb.induct)
paulson@18886
   258
apply auto
paulson@18886
   259
done
paulson@18886
   260
paulson@18886
   261
lemma Gets_imp_knows_Spy: 
paulson@18886
   262
     "\<lbrakk> Gets B X \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> X \<in> knows Spy evs"
paulson@18886
   263
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
paulson@18886
   264
done
paulson@18886
   265
paulson@18886
   266
lemma Gets_imp_knows_Spy_parts_Snd: 
paulson@18886
   267
     "\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> Y \<in> parts (knows Spy evs)"
paulson@18886
   268
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy parts.Inj parts.Snd)
paulson@18886
   269
done
paulson@18886
   270
paulson@18886
   271
lemma Gets_imp_knows_Spy_analz_Snd: 
paulson@18886
   272
     "\<lbrakk> Gets B \<lbrace>X, Y\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  \<Longrightarrow> Y \<in> analz (knows Spy evs)"
paulson@18886
   273
apply (blast dest!: Gets_imp_Says Says_imp_knows_Spy analz.Inj analz.Snd)
paulson@18886
   274
done
paulson@18886
   275
paulson@18886
   276
(*end general facts*)
paulson@18886
   277
paulson@18886
   278
paulson@18886
   279
wenzelm@24122
   280
(*Begin lemmas on secure means, from Event.thy, proved for shouprubin. They help
paulson@18886
   281
  the simplifier, especially in analz_image_freshK*)
paulson@18886
   282
paulson@18886
   283
paulson@18886
   284
lemma Inputs_imp_knows_Spy_secureM_srb: 
paulson@18886
   285
      "\<lbrakk> Inputs Spy C X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> X \<in> knows Spy evs"
paulson@18886
   286
apply (simp (no_asm_simp) add: Inputs_imp_knows_Spy_secureM)
paulson@18886
   287
done
paulson@18886
   288
paulson@18886
   289
lemma knows_Spy_Inputs_secureM_srb_Spy: 
paulson@18886
   290
      "evs \<in>srb \<Longrightarrow> knows Spy (Inputs Spy C X # evs) = insert X (knows Spy evs)"
paulson@18886
   291
apply (simp (no_asm_simp))
paulson@18886
   292
done
paulson@18886
   293
paulson@18886
   294
lemma knows_Spy_Inputs_secureM_srb: 
paulson@18886
   295
    "\<lbrakk> A \<noteq> Spy; evs \<in>srb \<rbrakk> \<Longrightarrow> knows Spy (Inputs A C X # evs) =  knows Spy evs"
paulson@18886
   296
apply (simp (no_asm_simp))
paulson@18886
   297
done
paulson@18886
   298
paulson@18886
   299
lemma knows_Spy_Outpts_secureM_srb_Spy: 
paulson@18886
   300
      "evs \<in>srb \<Longrightarrow> knows Spy (Outpts C Spy X # evs) = insert X (knows Spy evs)"
paulson@18886
   301
apply (simp (no_asm_simp))
paulson@18886
   302
done
paulson@18886
   303
paulson@18886
   304
lemma knows_Spy_Outpts_secureM_srb: 
paulson@18886
   305
     "\<lbrakk> A \<noteq> Spy; evs \<in>srb \<rbrakk> \<Longrightarrow> knows Spy (Outpts C A X # evs) =  knows Spy evs"
paulson@18886
   306
apply (simp (no_asm_simp))
paulson@18886
   307
done
paulson@18886
   308
paulson@18886
   309
(*End lemmas on secure means for shouprubin*)
paulson@18886
   310
paulson@18886
   311
paulson@18886
   312
paulson@18886
   313
paulson@18886
   314
(*BEGIN technical lemmas - evolution of forwarding lemmas*)
paulson@18886
   315
paulson@18886
   316
(*If an honest agent uses a smart card, then the card is his/her own, is
paulson@18886
   317
  not stolen, and the agent has received suitable data to feed the card. 
paulson@18886
   318
  In other words, these are guarantees that an honest agent can only use 
paulson@18886
   319
  his/her own card, and must use it correctly.
paulson@18886
   320
  On the contrary, the spy can "Inputs" any cloned cards also by the Fake rule.
paulson@18886
   321
paulson@18886
   322
  Instead of Auto_tac, proofs here used to asm-simplify and then force-tac.
paulson@18886
   323
*)
paulson@18886
   324
lemma Inputs_A_Card_3: 
paulson@18886
   325
    "\<lbrakk> Inputs A C (Agent A) \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   326
     \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   327
      (\<exists> Pk Certificate. Gets A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs)"
paulson@18886
   328
apply (erule rev_mp, erule srb.induct)
paulson@18886
   329
apply auto
paulson@18886
   330
done
paulson@18886
   331
paulson@18886
   332
lemma Inputs_B_Card_6: 
paulson@18886
   333
     "\<lbrakk> Inputs B C \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; B \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   334
      \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
paulson@18886
   335
apply (erule rev_mp, erule srb.induct)
paulson@18886
   336
apply auto
paulson@18886
   337
done
paulson@18886
   338
paulson@18886
   339
lemma Inputs_A_Card_9: 
paulson@18886
   340
     "\<lbrakk> Inputs A C \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
paulson@18886
   341
                                           Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
paulson@18886
   342
         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   343
  \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   344
      Gets A \<lbrace>Nonce Pk, Cert1\<rbrace> \<in> set evs     \<and>  
paulson@18886
   345
      Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace> \<in> set evs        \<and>   
paulson@18886
   346
      Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
paulson@18886
   347
apply (erule rev_mp, erule srb.induct)
paulson@18886
   348
apply auto
paulson@18886
   349
done
paulson@18886
   350
paulson@18886
   351
paulson@18886
   352
(*The two occurrences of A in the Outpts event don't match SR_U4Fake, where
paulson@18886
   353
  A cannot be the Spy. Hence the card is legally usable by rule SR_U4*)
paulson@18886
   354
lemma Outpts_A_Card_4: 
paulson@18886
   355
     "\<lbrakk> Outpts C A \<lbrace>Nonce Na, (Crypt (crdK (Card A)) (Nonce Na))\<rbrace> \<in> set evs;  
paulson@18886
   356
         evs \<in> srb \<rbrakk>  
paulson@18886
   357
     \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   358
         Inputs A (Card A) (Agent A) \<in> set evs"
paulson@18886
   359
apply (erule rev_mp, erule srb.induct)
paulson@18886
   360
apply auto
paulson@18886
   361
done
paulson@18886
   362
paulson@18886
   363
paulson@18886
   364
(*First certificate is made explicit so that a comment similar to the previous
paulson@18886
   365
  applies. This also provides Na to the Inputs event in the conclusion*)
paulson@18886
   366
lemma Outpts_B_Card_7: 
paulson@18886
   367
      "\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Agent A, Key K,  
paulson@18886
   368
                      Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
paulson@18886
   369
                      Cert2\<rbrace> \<in> set evs;  
paulson@18886
   370
         evs \<in> srb \<rbrakk>  
paulson@18886
   371
     \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>  
paulson@18886
   372
         Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
paulson@18886
   373
apply (erule rev_mp, erule srb.induct)
paulson@18886
   374
apply auto
paulson@18886
   375
done
paulson@18886
   376
paulson@18886
   377
lemma Outpts_A_Card_10: 
paulson@18886
   378
     "\<lbrakk> Outpts C A \<lbrace>Agent B, Nonce Nb, 
paulson@18886
   379
                    Key K, (Crypt (pairK(A,B)) (Nonce Nb))\<rbrace> \<in> set evs; 
paulson@18886
   380
         evs \<in> srb \<rbrakk>  
paulson@18886
   381
     \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   382
         (\<exists> Na Ver1 Ver2 Ver3.  
paulson@18886
   383
       Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
paulson@18886
   384
                              Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
paulson@18886
   385
apply (erule rev_mp, erule srb.induct)
paulson@18886
   386
apply auto
paulson@18886
   387
done
paulson@18886
   388
paulson@18886
   389
paulson@18886
   390
paulson@18886
   391
(*
paulson@18886
   392
Contrarily to original version, A doesn't need to check the form of the 
paulson@18886
   393
certificate to learn that her peer is B. The goal is available to A.
paulson@18886
   394
*)
paulson@18886
   395
lemma Outpts_A_Card_10_imp_Inputs: 
paulson@18886
   396
     "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
paulson@18886
   397
          \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   398
     \<Longrightarrow> (\<exists> Na Ver1 Ver2 Ver3.  
paulson@18886
   399
       Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),  
paulson@18886
   400
                              Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
paulson@18886
   401
apply (erule rev_mp, erule srb.induct)
paulson@18886
   402
apply simp_all
paulson@18886
   403
apply blast+
paulson@18886
   404
done
paulson@18886
   405
paulson@18886
   406
paulson@18886
   407
paulson@18886
   408
paulson@18886
   409
(*Weaker version: if the agent can't check the forms of the verifiers, then
paulson@18886
   410
  the agent must not be the spy so as to solve SR_U4Fake. The verifier must be
paulson@18886
   411
  recognised as some cyphertex in order to distinguish from case SR_U7, 
paulson@18886
   412
  concerning B's output, which also begins with a nonce.
paulson@18886
   413
*)
paulson@18886
   414
lemma Outpts_honest_A_Card_4: 
paulson@18886
   415
     "\<lbrakk> Outpts C A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in>set evs; 
paulson@18886
   416
         A \<noteq> Spy;  evs \<in> srb \<rbrakk>  
paulson@18886
   417
     \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   418
         Inputs A (Card A) (Agent A) \<in> set evs"
paulson@18886
   419
apply (erule rev_mp, erule srb.induct)
paulson@18886
   420
apply auto
paulson@18886
   421
done
paulson@18886
   422
paulson@18886
   423
(*alternative formulation of same theorem
paulson@18886
   424
Goal "\<lbrakk> Outpts C A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;  
paulson@18886
   425
         \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;    
paulson@18886
   426
         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   427
     \<Longrightarrow> legalUse(C) \<and> C = (Card A) \<and>  
paulson@18886
   428
         Inputs A (Card A) (Agent A) \<in> set evs"
paulson@18886
   429
same proof
paulson@18886
   430
*)
paulson@18886
   431
paulson@18886
   432
paulson@18886
   433
lemma Outpts_honest_B_Card_7: 
paulson@18886
   434
    "\<lbrakk> Outpts C B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;  
paulson@18886
   435
       B \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   436
   \<Longrightarrow> legalUse(C) \<and> C = (Card B) \<and>  
paulson@18886
   437
       (\<exists> Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs)"
paulson@18886
   438
apply (erule rev_mp, erule srb.induct)
paulson@18886
   439
apply auto
paulson@18886
   440
done
paulson@18886
   441
paulson@18886
   442
lemma Outpts_honest_A_Card_10: 
paulson@18886
   443
     "\<lbrakk> Outpts C A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;  
paulson@18886
   444
         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   445
     \<Longrightarrow> legalUse (C) \<and> C = (Card A) \<and>  
paulson@18886
   446
         (\<exists> Na Pk Ver1 Ver2 Ver3.  
paulson@18886
   447
          Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Pk,  
paulson@18886
   448
                              Ver1, Ver2, Ver3\<rbrace> \<in> set evs)"
paulson@18886
   449
apply (erule rev_mp, erule srb.induct)
paulson@18886
   450
apply simp_all
paulson@18886
   451
apply blast+
paulson@18886
   452
done
paulson@18886
   453
(*-END-*)
paulson@18886
   454
paulson@18886
   455
paulson@18886
   456
(*Even weaker versions: if the agent can't check the forms of the verifiers
paulson@18886
   457
  and the agent may be the spy, then we must know what card the agent
paulson@18886
   458
  is getting the output from. 
paulson@18886
   459
*)
paulson@18886
   460
lemma Outpts_which_Card_4: 
paulson@18886
   461
    "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt K X\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   462
    \<Longrightarrow> Inputs A (Card A) (Agent A) \<in> set evs"
paulson@18886
   463
apply (erule rev_mp, erule srb.induct)
paulson@18886
   464
apply (simp_all (no_asm_simp))
paulson@18886
   465
apply clarify
paulson@18886
   466
done
paulson@18886
   467
paulson@18886
   468
lemma Outpts_which_Card_7: 
paulson@18886
   469
  "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
paulson@18886
   470
       \<in> set evs;  evs \<in> srb \<rbrakk>  
paulson@18886
   471
     \<Longrightarrow> \<exists> Na. Inputs B (Card B) \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
paulson@18886
   472
apply (erule rev_mp, erule srb.induct)
paulson@18886
   473
apply auto
paulson@18886
   474
done
paulson@18886
   475
paulson@18886
   476
(*This goal is now available - in the sense of Goal Availability*)
paulson@18886
   477
lemma Outpts_which_Card_10: 
paulson@18886
   478
    "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate \<rbrace> \<in> set evs;
paulson@18886
   479
       evs \<in> srb \<rbrakk>  
paulson@18886
   480
    \<Longrightarrow> \<exists> Na. Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)), 
paulson@18886
   481
                            Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>,  
paulson@18886
   482
                            Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
paulson@18886
   483
                            Crypt (crdK (Card A)) (Nonce Na) \<rbrace> \<in> set evs"
paulson@18886
   484
apply (erule rev_mp, erule srb.induct)
paulson@18886
   485
apply auto
paulson@18886
   486
done
paulson@18886
   487
paulson@18886
   488
paulson@18886
   489
(*Lemmas on the form of outputs*)
paulson@18886
   490
paulson@18886
   491
paulson@18886
   492
(*A needs to check that the verifier is a cipher for it to come from SR_U4
paulson@18886
   493
  otherwise it could come from SR_U7 *)
paulson@18886
   494
lemma Outpts_A_Card_form_4: 
paulson@18886
   495
  "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Certificate\<rbrace> \<in> set evs;  
paulson@18886
   496
         \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>; evs \<in> srb \<rbrakk>  
paulson@18886
   497
     \<Longrightarrow> Certificate = (Crypt (crdK (Card A)) (Nonce Na))"
paulson@18886
   498
apply (erule rev_mp, erule srb.induct)
paulson@18886
   499
apply (simp_all (no_asm_simp))
paulson@18886
   500
done
paulson@18886
   501
paulson@18886
   502
lemma Outpts_B_Card_form_7: 
paulson@18886
   503
   "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
paulson@18886
   504
        \<in> set evs; evs \<in> srb \<rbrakk>          
paulson@18886
   505
      \<Longrightarrow> \<exists> Na.    
paulson@18886
   506
          K = sesK(Nb,pairK(A,B)) \<and>                       
paulson@18886
   507
          Cert1 = (Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>) \<and>  
paulson@18886
   508
          Cert2 = (Crypt (pairK(A,B)) (Nonce Nb))"
paulson@18886
   509
apply (erule rev_mp, erule srb.induct)
paulson@18886
   510
apply auto
paulson@18886
   511
done
paulson@18886
   512
paulson@18886
   513
lemma Outpts_A_Card_form_10: 
paulson@18886
   514
   "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> 
paulson@18886
   515
        \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   516
      \<Longrightarrow> K = sesK(Nb,pairK(A,B)) \<and>  
paulson@18886
   517
          Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
paulson@18886
   518
apply (erule rev_mp, erule srb.induct)
paulson@18886
   519
apply (simp_all (no_asm_simp))
paulson@18886
   520
done
paulson@18886
   521
paulson@18886
   522
lemma Outpts_A_Card_form_bis: 
paulson@18886
   523
  "\<lbrakk> Outpts (Card A') A' \<lbrace>Agent B', Nonce Nb', Key (sesK(Nb,pairK(A,B))), 
paulson@18886
   524
     Certificate\<rbrace> \<in> set evs; 
paulson@18886
   525
         evs \<in> srb \<rbrakk>  
paulson@18886
   526
      \<Longrightarrow> A' = A \<and> B' = B \<and> Nb = Nb' \<and>  
paulson@18886
   527
          Certificate = (Crypt (pairK(A,B)) (Nonce Nb))"
paulson@18886
   528
apply (erule rev_mp, erule srb.induct)
paulson@18886
   529
apply (simp_all (no_asm_simp))
paulson@18886
   530
done
paulson@18886
   531
paulson@18886
   532
(*\<dots> and Inputs *)
paulson@18886
   533
paulson@18886
   534
lemma Inputs_A_Card_form_9: 
paulson@18886
   535
paulson@18886
   536
     "\<lbrakk> Inputs A (Card A) \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk,   
paulson@18886
   537
                             Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
paulson@18886
   538
         evs \<in> srb \<rbrakk>  
paulson@18886
   539
  \<Longrightarrow>    Cert3 = Crypt (crdK (Card A)) (Nonce Na)"
paulson@18886
   540
apply (erule rev_mp)
paulson@18886
   541
apply (erule srb.induct)
paulson@18886
   542
apply (simp_all (no_asm_simp))
paulson@18886
   543
(*Fake*)
paulson@18886
   544
apply force
paulson@18886
   545
(*SR_U9*)
paulson@18886
   546
apply (blast dest!: Outpts_A_Card_form_4)
paulson@18886
   547
done
paulson@18886
   548
(* Pk, Cert1, Cert2 cannot be made explicit because they traversed the network in the clear *)
paulson@18886
   549
paulson@18886
   550
paulson@18886
   551
paulson@18886
   552
(*General guarantees on Inputs and Outpts*)
paulson@18886
   553
paulson@18886
   554
(*for any agents*)
paulson@18886
   555
paulson@18886
   556
paulson@18886
   557
lemma Inputs_Card_legalUse: 
paulson@18886
   558
  "\<lbrakk> Inputs A (Card A) X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> legalUse(Card A)"
paulson@18886
   559
apply (erule rev_mp, erule srb.induct)
paulson@18886
   560
apply auto
paulson@18886
   561
done
paulson@18886
   562
paulson@18886
   563
lemma Outpts_Card_legalUse: 
paulson@18886
   564
  "\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> legalUse(Card A)"
paulson@18886
   565
apply (erule rev_mp, erule srb.induct)
paulson@18886
   566
apply auto
paulson@18886
   567
done
paulson@18886
   568
paulson@18886
   569
(*for honest agents*)
paulson@18886
   570
paulson@18886
   571
lemma Inputs_Card: "\<lbrakk> Inputs A C X \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   572
      \<Longrightarrow> C = (Card A) \<and> legalUse(C)"
paulson@18886
   573
apply (erule rev_mp, erule srb.induct)
paulson@18886
   574
apply auto
paulson@18886
   575
done
paulson@18886
   576
paulson@18886
   577
lemma Outpts_Card: "\<lbrakk> Outpts C A X \<in> set evs; A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   578
      \<Longrightarrow> C = (Card A) \<and> legalUse(C)"
paulson@18886
   579
apply (erule rev_mp, erule srb.induct)
paulson@18886
   580
apply auto
paulson@18886
   581
done
paulson@18886
   582
paulson@18886
   583
lemma Inputs_Outpts_Card: 
paulson@18886
   584
     "\<lbrakk> Inputs A C X \<in> set evs \<or> Outpts C A Y \<in> set evs;  
paulson@18886
   585
         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
   586
     \<Longrightarrow> C = (Card A) \<and> legalUse(Card A)"
paulson@18886
   587
apply (blast dest: Inputs_Card Outpts_Card)
paulson@18886
   588
done
paulson@18886
   589
paulson@18886
   590
paulson@18886
   591
(*for the spy - they stress that the model behaves as it is meant to*) 
paulson@18886
   592
paulson@18886
   593
(*The or version can be also proved directly.
paulson@18886
   594
  It stresses that the spy may use either her own legally usable card or
paulson@18886
   595
  all the illegally usable cards.
paulson@18886
   596
*)
paulson@18886
   597
lemma Inputs_Card_Spy: 
paulson@18886
   598
  "\<lbrakk> Inputs Spy C X \<in> set evs \<or> Outpts C Spy X \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   599
      \<Longrightarrow> C = (Card Spy) \<and> legalUse(Card Spy) \<or>  
paulson@18886
   600
          (\<exists> A. C = (Card A) \<and> illegalUse(Card A))"
paulson@18886
   601
apply (erule rev_mp, erule srb.induct)
paulson@18886
   602
apply auto
paulson@18886
   603
done
paulson@18886
   604
paulson@18886
   605
paulson@18886
   606
(*END technical lemmas*)
paulson@18886
   607
paulson@18886
   608
paulson@18886
   609
paulson@18886
   610
paulson@18886
   611
paulson@18886
   612
paulson@18886
   613
(*BEGIN unicity theorems: certain items uniquely identify a smart card's
paulson@18886
   614
                          output*)
paulson@18886
   615
paulson@18886
   616
(*A's card's first output: the nonce uniquely identifies the rest*)
paulson@18886
   617
lemma Outpts_A_Card_unique_nonce:
paulson@18886
   618
     "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace>  
paulson@18886
   619
           \<in> set evs;   
paulson@18886
   620
         Outpts (Card A') A' \<lbrace>Nonce Na, Crypt (crdK (Card A')) (Nonce Na)\<rbrace> 
paulson@18886
   621
           \<in> set evs;   
paulson@18886
   622
         evs \<in> srb \<rbrakk> \<Longrightarrow> A=A'"
paulson@18886
   623
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
paulson@18886
   624
apply (fastsimp dest: Outpts_parts_used)
paulson@18886
   625
apply blast
paulson@18886
   626
done
paulson@18886
   627
paulson@18886
   628
(*B's card's output: the NONCE uniquely identifies the rest*)
paulson@18886
   629
lemma Outpts_B_Card_unique_nonce: 
paulson@18886
   630
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;   
paulson@18886
   631
      Outpts (Card B') B' \<lbrace>Nonce Nb, Agent A', Key SK', Cert1', Cert2'\<rbrace> \<in> set evs;
paulson@18886
   632
       evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> SK=SK' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
paulson@18886
   633
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
paulson@18886
   634
apply (fastsimp dest: Outpts_parts_used)
paulson@18886
   635
apply blast
paulson@18886
   636
done
paulson@18886
   637
paulson@18886
   638
paulson@18886
   639
(*B's card's output: the SESKEY uniquely identifies the rest*)
paulson@18886
   640
lemma Outpts_B_Card_unique_key: 
paulson@18886
   641
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key SK, Cert1, Cert2\<rbrace> \<in> set evs;   
paulson@18886
   642
      Outpts (Card B') B' \<lbrace>Nonce Nb', Agent A', Key SK, Cert1', Cert2'\<rbrace> \<in> set evs; 
paulson@18886
   643
       evs \<in> srb \<rbrakk> \<Longrightarrow> B=B' \<and> A=A' \<and> Nb=Nb' \<and> Cert1=Cert1' \<and> Cert2=Cert2'"
paulson@18886
   644
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
paulson@18886
   645
apply (fastsimp dest: Outpts_parts_used)
paulson@18886
   646
apply blast
paulson@18886
   647
done
paulson@18886
   648
paulson@18886
   649
lemma Outpts_A_Card_unique_key: 
paulson@18886
   650
   "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, V\<rbrace> \<in> set evs;   
paulson@18886
   651
      Outpts (Card A') A' \<lbrace>Agent B', Nonce Nb', Key K, V'\<rbrace> \<in> set evs;   
paulson@18886
   652
         evs \<in> srb \<rbrakk> \<Longrightarrow> A=A' \<and> B=B' \<and> Nb=Nb' \<and> V=V'"
paulson@18886
   653
apply (erule rev_mp, erule rev_mp, erule srb.induct, simp_all)
paulson@18886
   654
apply (blast dest: Outpts_A_Card_form_bis)
paulson@18886
   655
apply blast
paulson@18886
   656
done
paulson@18886
   657
paulson@18886
   658
paulson@18886
   659
(*Revised unicity theorem - applies to both steps 4 and 7*)
paulson@18886
   660
lemma Outpts_A_Card_Unique: 
paulson@18886
   661
  "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   662
     \<Longrightarrow> Unique (Outpts (Card A) A \<lbrace>Nonce Na, rest\<rbrace>) on evs"
paulson@18886
   663
apply (erule rev_mp, erule srb.induct, simp_all add: Unique_def)
paulson@18886
   664
apply (fastsimp dest: Outpts_parts_used)
paulson@18886
   665
apply blast
paulson@18886
   666
apply (fastsimp dest: Outpts_parts_used)
paulson@18886
   667
apply blast
paulson@18886
   668
done
paulson@18886
   669
paulson@18886
   670
(*can't prove the same on evs10 for it doesn't have a freshness assumption!*)
paulson@18886
   671
paulson@18886
   672
paulson@18886
   673
(*END unicity theorems*)
paulson@18886
   674
paulson@18886
   675
paulson@18886
   676
(*BEGIN counterguarantees about spy's knowledge*)
paulson@18886
   677
paulson@18886
   678
(*on nonces*)
paulson@18886
   679
paulson@18886
   680
lemma Spy_knows_Na: 
paulson@18886
   681
      "\<lbrakk> Says A B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   682
      \<Longrightarrow> Nonce Na \<in> analz (knows Spy evs)"
paulson@18886
   683
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Snd])
paulson@18886
   684
done
paulson@18886
   685
paulson@18886
   686
lemma Spy_knows_Nb: 
paulson@18886
   687
      "\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   688
      \<Longrightarrow> Nonce Nb \<in> analz (knows Spy evs)"
paulson@18886
   689
apply (blast dest!: Says_imp_knows_Spy [THEN analz.Inj, THEN analz.Fst])
paulson@18886
   690
done
paulson@18886
   691
paulson@18886
   692
paulson@18886
   693
(*on Pairkey*)
paulson@18886
   694
paulson@18886
   695
lemma Pairkey_Gets_analz_knows_Spy: 
paulson@18886
   696
      "\<lbrakk> Gets A \<lbrace>Nonce (Pairkey(A,B)), Certificate\<rbrace> \<in> set evs; evs \<in> srb \<rbrakk>  
paulson@18886
   697
      \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
paulson@18886
   698
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
paulson@18886
   699
done
paulson@18886
   700
paulson@18886
   701
lemma Pairkey_Inputs_imp_Gets: 
paulson@18886
   702
     "\<lbrakk> Inputs A (Card A)             
paulson@18886
   703
           \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
paulson@18886
   704
             Cert1, Cert3, Cert2\<rbrace> \<in> set evs;           
paulson@18886
   705
         A \<noteq> Spy; evs \<in> srb \<rbrakk>     
paulson@18886
   706
      \<Longrightarrow> Gets A \<lbrace>Nonce (Pairkey(A,B)), Cert1\<rbrace> \<in> set evs"
paulson@18886
   707
apply (erule rev_mp, erule srb.induct)
paulson@18886
   708
apply (simp_all (no_asm_simp))
paulson@18886
   709
apply force
paulson@18886
   710
done
paulson@18886
   711
paulson@18886
   712
lemma Pairkey_Inputs_analz_knows_Spy: 
paulson@18886
   713
     "\<lbrakk> Inputs A (Card A)             
paulson@18886
   714
           \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce (Pairkey(A,B)),     
paulson@18886
   715
             Cert1, Cert3, Cert2\<rbrace> \<in> set evs;           
paulson@18886
   716
         evs \<in> srb \<rbrakk>     
paulson@18886
   717
     \<Longrightarrow> Nonce (Pairkey(A,B)) \<in> analz (knows Spy evs)"
paulson@18886
   718
apply (case_tac "A = Spy")
paulson@18886
   719
apply (fastsimp dest!: Inputs_imp_knows_Spy_secureM [THEN analz.Inj])
paulson@18886
   720
apply (blast dest!: Pairkey_Inputs_imp_Gets [THEN Pairkey_Gets_analz_knows_Spy])
paulson@18886
   721
done
paulson@18886
   722
paulson@18886
   723
(* This fails on base case because of XOR properties.
paulson@18886
   724
lemma Pairkey_authentic:
paulson@18886
   725
  "\<lbrakk> Nonce (Pairkey(A,B)) \<in> parts (knows Spy evs);
paulson@18886
   726
     Card A \<notin> cloned; evs \<in> sr \<rbrakk>
paulson@18886
   727
 \<Longrightarrow> \<exists> cert. Says Server A \<lbrace>Nonce (Pairkey(A,B)), Cert\<rbrace> \<in> set evs"
paulson@18886
   728
apply (erule rev_mp)
paulson@18886
   729
apply (erule sr.induct, simp_all)
paulson@18886
   730
apply clarify
paulson@18886
   731
oops
paulson@18886
   732
paulson@18886
   733
 1. \<And>x a b.
paulson@18886
   734
       \<lbrakk>Card A \<notin> cloned; Pairkey (A, B) = Pairkey (a, b); Card a \<in> cloned;
paulson@18886
   735
        Card b \<in> cloned\<rbrakk>
paulson@18886
   736
       \<Longrightarrow> False
paulson@18886
   737
*)
paulson@18886
   738
paulson@18886
   739
paulson@18886
   740
(*END counterguarantees on spy's knowledge*)
paulson@18886
   741
paulson@18886
   742
paulson@18886
   743
(*BEGIN rewrite rules for parts operator*)
paulson@18886
   744
paulson@18886
   745
declare shrK_disj_sesK [THEN not_sym, iff] 
paulson@18886
   746
declare pin_disj_sesK [THEN not_sym, iff]
paulson@18886
   747
declare crdK_disj_sesK [THEN not_sym, iff]
paulson@18886
   748
declare pairK_disj_sesK [THEN not_sym, iff]
paulson@18886
   749
paulson@18886
   750
paulson@18886
   751
ML
paulson@18886
   752
{*
wenzelm@24122
   753
structure ShoupRubinBella =
wenzelm@24122
   754
struct
paulson@18886
   755
wenzelm@23894
   756
fun prepare_tac ctxt = 
wenzelm@24122
   757
 (*SR_U8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
wenzelm@23894
   758
 (*SR_U8*)   clarify_tac (local_claset_of ctxt) 15 THEN
wenzelm@24122
   759
 (*SR_U9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
wenzelm@24122
   760
 (*SR_U11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 
paulson@18886
   761
wenzelm@23894
   762
fun parts_prepare_tac ctxt = 
wenzelm@23894
   763
           prepare_tac ctxt THEN
wenzelm@24122
   764
 (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 18 THEN 
wenzelm@24122
   765
 (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
wenzelm@24122
   766
 (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
wenzelm@24122
   767
 (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
wenzelm@23894
   768
 (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
paulson@18886
   769
wenzelm@23894
   770
fun analz_prepare_tac ctxt = 
wenzelm@23894
   771
         prepare_tac ctxt THEN
wenzelm@24122
   772
         dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN 
wenzelm@24122
   773
 (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN 
paulson@18886
   774
         REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
paulson@18886
   775
wenzelm@24122
   776
end
paulson@18886
   777
*}
paulson@18886
   778
paulson@18886
   779
method_setup prepare = {*
wenzelm@30549
   780
    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.prepare_tac ctxt)) *}
paulson@18886
   781
  "to launch a few simple facts that'll help the simplifier"
paulson@18886
   782
paulson@18886
   783
method_setup parts_prepare = {*
wenzelm@30549
   784
    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.parts_prepare_tac ctxt)) *}
paulson@18886
   785
  "additional facts to reason about parts"
paulson@18886
   786
paulson@18886
   787
method_setup analz_prepare = {*
wenzelm@30549
   788
    Scan.succeed (fn ctxt => SIMPLE_METHOD (ShoupRubinBella.analz_prepare_tac ctxt)) *}
paulson@18886
   789
  "additional facts to reason about analz"
paulson@18886
   790
paulson@18886
   791
paulson@18886
   792
paulson@18886
   793
lemma Spy_parts_keys [simp]: "evs \<in> srb \<Longrightarrow>  
paulson@18886
   794
  (Key (shrK P) \<in> parts (knows Spy evs)) = (Card P \<in> cloned) \<and>  
paulson@18886
   795
  (Key (pin P) \<in> parts (knows Spy evs)) = (P \<in> bad \<or> Card P \<in> cloned) \<and>  
paulson@18886
   796
  (Key (crdK C) \<in> parts (knows Spy evs)) = (C \<in> cloned) \<and>  
paulson@18886
   797
  (Key (pairK(A,B)) \<in> parts (knows Spy evs)) = (Card B \<in> cloned)"
paulson@18886
   798
apply (erule srb.induct)
paulson@18886
   799
apply parts_prepare
paulson@18886
   800
apply simp_all
paulson@18886
   801
apply (blast intro: parts_insertI)
paulson@18886
   802
done
paulson@18886
   803
paulson@18886
   804
(*END rewrite rules for parts operator*)
paulson@18886
   805
paulson@18886
   806
(*BEGIN rewrite rules for analz operator*)
paulson@18886
   807
paulson@18886
   808
paulson@18886
   809
lemma Spy_analz_shrK[simp]: "evs \<in> srb \<Longrightarrow>  
paulson@18886
   810
  (Key (shrK P) \<in> analz (knows Spy evs)) = (Card P \<in> cloned)"
paulson@18886
   811
apply (auto dest!: Spy_knows_cloned)
paulson@18886
   812
done
paulson@18886
   813
paulson@18886
   814
lemma Spy_analz_crdK[simp]: "evs \<in> srb \<Longrightarrow>  
paulson@18886
   815
  (Key (crdK C) \<in> analz (knows Spy evs)) = (C \<in> cloned)"
paulson@18886
   816
apply (auto dest!: Spy_knows_cloned)
paulson@18886
   817
done
paulson@18886
   818
paulson@18886
   819
lemma Spy_analz_pairK[simp]: "evs \<in> srb \<Longrightarrow>  
paulson@18886
   820
  (Key (pairK(A,B)) \<in> analz (knows Spy evs)) = (Card B \<in> cloned)"
paulson@18886
   821
apply (auto dest!: Spy_knows_cloned)
paulson@18886
   822
done
paulson@18886
   823
paulson@18886
   824
paulson@18886
   825
paulson@18886
   826
paulson@18886
   827
(*Because initState contains a set of nonces, this is needed for base case of
paulson@18886
   828
  analz_image_freshK*)
paulson@18886
   829
lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
paulson@18886
   830
apply auto
paulson@18886
   831
done
paulson@18886
   832
paulson@18886
   833
method_setup sc_analz_freshK = {*
wenzelm@30549
   834
    Scan.succeed (fn ctxt =>
wenzelm@30510
   835
     (SIMPLE_METHOD
wenzelm@21588
   836
      (EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
wenzelm@24122
   837
          REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
wenzelm@24122
   838
          ALLGOALS (asm_simp_tac (Simplifier.context ctxt Smartcard.analz_image_freshK_ss
wenzelm@24122
   839
              addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy},
wenzelm@24122
   840
                  @{thm knows_Spy_Outpts_secureM_srb_Spy},
wenzelm@24122
   841
                  @{thm shouprubin_assumes_securemeans},
wenzelm@24122
   842
                  @{thm analz_image_Key_Un_Nonce}]))]))) *}
paulson@18886
   843
    "for proving the Session Key Compromise theorem for smartcard protocols"
paulson@18886
   844
paulson@18886
   845
paulson@18886
   846
lemma analz_image_freshK [rule_format]: 
paulson@18886
   847
     "evs \<in> srb \<Longrightarrow>      \<forall> K KK.  
paulson@18886
   848
          (Key K \<in> analz (Key`KK \<union> (knows Spy evs))) =  
paulson@18886
   849
          (K \<in> KK \<or> Key K \<in> analz (knows Spy evs))"
paulson@18886
   850
apply (erule srb.induct)
paulson@18886
   851
apply analz_prepare
paulson@18886
   852
apply sc_analz_freshK
paulson@18886
   853
apply spy_analz
paulson@18886
   854
done
paulson@18886
   855
paulson@18886
   856
paulson@18886
   857
lemma analz_insert_freshK: "evs \<in> srb \<Longrightarrow>   
paulson@18886
   858
         Key K \<in> analz (insert (Key K') (knows Spy evs)) =  
paulson@18886
   859
         (K = K' \<or> Key K \<in> analz (knows Spy evs))"
paulson@18886
   860
apply (simp only: analz_image_freshK_simps analz_image_freshK)
paulson@18886
   861
done
paulson@18886
   862
paulson@18886
   863
(*END rewrite rules for analz operator*)
paulson@18886
   864
paulson@18886
   865
(*BEGIN authenticity theorems*)
paulson@18886
   866
paulson@18886
   867
paulson@18886
   868
paulson@18886
   869
paulson@18886
   870
lemma Na_Nb_certificate_authentic: 
paulson@18886
   871
     "\<lbrakk> Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs);  
paulson@18886
   872
         \<not>illegalUse(Card B); 
paulson@18886
   873
         evs \<in> srb \<rbrakk>           
paulson@18886
   874
     \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
paulson@18886
   875
                Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   876
                Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
   877
apply (erule rev_mp, erule srb.induct)
paulson@18886
   878
apply parts_prepare
paulson@18886
   879
apply simp_all
paulson@18886
   880
(*Fake*)
paulson@18886
   881
apply spy_analz
paulson@18886
   882
(*SR_U7F*)
paulson@18886
   883
apply clarify
paulson@18886
   884
(*SR_U8*)
paulson@18886
   885
apply clarify
paulson@18886
   886
done
paulson@18886
   887
paulson@18886
   888
lemma Nb_certificate_authentic:
paulson@18886
   889
      "\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);  
paulson@18886
   890
         B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
   891
         evs \<in> srb \<rbrakk>    
paulson@18886
   892
     \<Longrightarrow> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key (sesK(Nb,pairK(A,B))),  
paulson@18886
   893
                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
   894
apply (erule rev_mp, erule srb.induct)
paulson@18886
   895
apply parts_prepare
paulson@18886
   896
apply (case_tac [17] "Aa = Spy")
paulson@18886
   897
apply simp_all
paulson@18886
   898
(*Fake*)
paulson@18886
   899
apply spy_analz
paulson@18886
   900
(*SR_U7F, SR_U10F*)
paulson@18886
   901
apply clarify+
paulson@18886
   902
done
paulson@18886
   903
paulson@18886
   904
paulson@18886
   905
paulson@18886
   906
(*Discovering the very origin of the Nb certificate...*)
paulson@18886
   907
lemma Outpts_A_Card_imp_pairK_parts: 
paulson@18886
   908
     "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, 
paulson@18886
   909
                    Key K, Certificate\<rbrace> \<in> set evs;  
paulson@18886
   910
        evs \<in> srb \<rbrakk>   
paulson@18886
   911
    \<Longrightarrow> \<exists> Na. Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace> \<in> parts (knows Spy evs)"
paulson@18886
   912
apply (erule rev_mp, erule srb.induct)
paulson@18886
   913
apply parts_prepare
paulson@18886
   914
apply simp_all
paulson@18886
   915
(*Fake*)
paulson@18886
   916
apply (blast dest: parts_insertI)
paulson@18886
   917
(*SR_U7*)
paulson@18886
   918
apply force
paulson@18886
   919
(*SR_U7F*)
paulson@18886
   920
apply force
paulson@18886
   921
(*SR_U8*)
paulson@18886
   922
apply blast
paulson@18886
   923
(*SR_U10*)
paulson@18886
   924
apply (blast dest: Inputs_imp_knows_Spy_secureM_srb parts.Inj Inputs_A_Card_9 Gets_imp_knows_Spy elim: knows_Spy_partsEs)
paulson@18886
   925
(*SR_U10F*)
paulson@18886
   926
apply (blast dest: Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] 
paulson@18886
   927
                   Inputs_A_Card_9 Gets_imp_knows_Spy 
paulson@18886
   928
             elim: knows_Spy_partsEs)
paulson@18886
   929
done
paulson@18886
   930
paulson@18886
   931
               
paulson@18886
   932
lemma Nb_certificate_authentic_bis: 
paulson@18886
   933
     "\<lbrakk> Crypt (pairK(A,B)) (Nonce Nb) \<in> parts (knows Spy evs);  
paulson@18886
   934
         B \<noteq> Spy; \<not>illegalUse(Card B); 
paulson@18886
   935
         evs \<in> srb \<rbrakk>    
paulson@18886
   936
 \<Longrightarrow> \<exists> Na. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
paulson@18886
   937
                   Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
   938
                   Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
   939
apply (erule rev_mp, erule srb.induct)
paulson@18886
   940
apply parts_prepare
paulson@18886
   941
apply (simp_all (no_asm_simp))
paulson@18886
   942
(*Fake*)
paulson@18886
   943
apply spy_analz
paulson@18886
   944
(*SR_U7*)
paulson@18886
   945
apply blast
paulson@18886
   946
(*SR_U7F*)
paulson@18886
   947
apply blast
paulson@18886
   948
(*SR_U8*)
paulson@18886
   949
apply force
paulson@18886
   950
(*SR_U10*)
paulson@18886
   951
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] elim: knows_Spy_partsEs)
paulson@18886
   952
(*SR_U10F*)
paulson@18886
   953
apply (blast dest: Na_Nb_certificate_authentic Inputs_imp_knows_Spy_secureM_srb [THEN parts.Inj] elim: knows_Spy_partsEs)
paulson@18886
   954
(*SR_U11*)
paulson@18886
   955
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_imp_pairK_parts)
paulson@18886
   956
done
paulson@18886
   957
paulson@18886
   958
paulson@18886
   959
lemma Pairkey_certificate_authentic: 
paulson@18886
   960
    "\<lbrakk> Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace> \<in> parts (knows Spy evs);    
paulson@18886
   961
         Card A \<notin> cloned; evs \<in> srb \<rbrakk>        
paulson@18886
   962
     \<Longrightarrow> Pk = Pairkey(A,B) \<and>              
paulson@18886
   963
         Says Server A \<lbrace>Nonce Pk,  
paulson@18886
   964
                        Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace> 
paulson@18886
   965
           \<in> set evs"
paulson@18886
   966
apply (erule rev_mp, erule srb.induct)
paulson@18886
   967
apply parts_prepare
paulson@18886
   968
apply (simp_all (no_asm_simp))
paulson@18886
   969
(*Fake*)
paulson@18886
   970
apply spy_analz
paulson@18886
   971
(*SR_U8*)
paulson@18886
   972
apply force
paulson@18886
   973
done
paulson@18886
   974
paulson@18886
   975
paulson@18886
   976
lemma sesK_authentic: 
paulson@18886
   977
     "\<lbrakk> Key (sesK(Nb,pairK(A,B))) \<in> parts (knows Spy evs);  
paulson@18886
   978
         A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
   979
         evs \<in> srb \<rbrakk>           
paulson@18886
   980
      \<Longrightarrow> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>  
paulson@18886
   981
           \<in> set evs"
paulson@18886
   982
apply (erule rev_mp, erule srb.induct)
paulson@18886
   983
apply parts_prepare
paulson@18886
   984
apply (simp_all)
paulson@18886
   985
(*fake*)
paulson@18886
   986
apply spy_analz
paulson@18886
   987
(*forge*)
paulson@18886
   988
apply (fastsimp dest: analz.Inj)
paulson@18886
   989
(*SR_U7: used B\<noteq>Spy*)
paulson@18886
   990
(*SR_U7F*)
paulson@18886
   991
apply clarify
paulson@18886
   992
(*SR_U10: used A\<noteq>Spy*)
paulson@18886
   993
(*SR_U10F*)
paulson@18886
   994
apply clarify
paulson@18886
   995
done
paulson@18886
   996
paulson@18886
   997
paulson@18886
   998
(*END authenticity theorems*)
paulson@18886
   999
paulson@18886
  1000
paulson@18886
  1001
(*BEGIN confidentiality theorems*)
paulson@18886
  1002
paulson@18886
  1003
paulson@18886
  1004
lemma Confidentiality: 
paulson@18886
  1005
     "\<lbrakk> Notes Spy \<lbrace>Key (sesK(Nb,pairK(A,B))), Nonce Nb, Agent A, Agent B\<rbrace>  
paulson@18886
  1006
           \<notin> set evs; 
paulson@18886
  1007
        A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
  1008
        evs \<in> srb \<rbrakk>           
paulson@18886
  1009
      \<Longrightarrow> Key (sesK(Nb,pairK(A,B))) \<notin> analz (knows Spy evs)"
paulson@18886
  1010
apply (blast intro: sesK_authentic)
paulson@18886
  1011
done
paulson@18886
  1012
paulson@18886
  1013
lemma Confidentiality_B: 
paulson@18886
  1014
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
paulson@18886
  1015
          \<in> set evs;  
paulson@18886
  1016
        Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;  
paulson@18886
  1017
        A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); Card B \<notin> cloned; 
paulson@18886
  1018
        evs \<in> srb \<rbrakk>  
paulson@18886
  1019
      \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
paulson@18886
  1020
apply (erule rev_mp, erule rev_mp, erule srb.induct)
paulson@18886
  1021
apply analz_prepare
paulson@18886
  1022
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
paulson@18886
  1023
(*Fake*)
paulson@18886
  1024
apply spy_analz
paulson@18886
  1025
(*Forge*)
paulson@18886
  1026
apply (rotate_tac 7)
paulson@18886
  1027
apply (drule parts.Inj)
paulson@18886
  1028
apply (fastsimp dest: Outpts_B_Card_form_7)
paulson@18886
  1029
(*SR_U7*)
paulson@18886
  1030
apply (blast dest!: Outpts_B_Card_form_7)
paulson@18886
  1031
(*SR_U7F*)
paulson@18886
  1032
apply clarify
paulson@18886
  1033
apply (drule Outpts_parts_used)
paulson@18886
  1034
apply simp
paulson@18886
  1035
(*faster than
paulson@18886
  1036
  by (fast_tac (claset() addDs [Outpts_parts_used] addss (simpset())) 1)
paulson@18886
  1037
*)
paulson@18886
  1038
(*SR_U10*)
paulson@18886
  1039
apply (fastsimp dest: Outpts_B_Card_form_7)
paulson@18886
  1040
(*SR_U10F - uses assumption Card A not cloned*)
paulson@18886
  1041
apply clarify
paulson@18886
  1042
apply (drule Outpts_B_Card_form_7, assumption)
paulson@18886
  1043
apply simp
paulson@18886
  1044
(*Oops1*)
paulson@18886
  1045
apply (blast dest!: Outpts_B_Card_form_7)
paulson@18886
  1046
(*Oops2*)
paulson@18886
  1047
apply (blast dest!: Outpts_B_Card_form_7 Outpts_A_Card_form_10)
paulson@18886
  1048
done
paulson@18886
  1049
paulson@18886
  1050
paulson@18886
  1051
(*END confidentiality theorems*)
paulson@18886
  1052
paulson@18886
  1053
paulson@18886
  1054
(*BEGIN authentication theorems*)
paulson@18886
  1055
paulson@18886
  1056
lemma A_authenticates_B: 
paulson@18886
  1057
     "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;
paulson@18886
  1058
        \<not>illegalUse(Card B); 
paulson@18886
  1059
        evs \<in> srb \<rbrakk>           
paulson@18886
  1060
 \<Longrightarrow> \<exists> Na. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,   
paulson@18886
  1061
                Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
  1062
                Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
  1063
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
paulson@18886
  1064
done
paulson@18886
  1065
paulson@18886
  1066
lemma A_authenticates_B_Gets: 
paulson@18886
  1067
     "\<lbrakk> Gets A \<lbrace>Nonce Nb, Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>\<rbrace>  
paulson@18886
  1068
           \<in> set evs;  
paulson@18886
  1069
         \<not>illegalUse(Card B); 
paulson@18886
  1070
         evs \<in> srb \<rbrakk>           
paulson@18886
  1071
    \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb, pairK (A, B))),   
paulson@18886
  1072
                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
  1073
                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
  1074
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
paulson@18886
  1075
done
paulson@18886
  1076
paulson@18886
  1077
paulson@18886
  1078
lemma A_authenticates_B_bis: 
paulson@18886
  1079
     "\<lbrakk> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Cert2\<rbrace> \<in> set evs;  
paulson@18886
  1080
        \<not>illegalUse(Card B); 
paulson@18886
  1081
        evs \<in> srb \<rbrakk>           
paulson@18886
  1082
 \<Longrightarrow> \<exists> Cert1. Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> 
paulson@18886
  1083
                \<in> set evs"
paulson@18886
  1084
apply (blast dest: Na_Nb_certificate_authentic Outpts_A_Card_form_10 Outpts_A_Card_imp_pairK_parts)
paulson@18886
  1085
done
paulson@18886
  1086
paulson@18886
  1087
paulson@18886
  1088
paulson@18886
  1089
paulson@18886
  1090
paulson@18886
  1091
paulson@18886
  1092
lemma B_authenticates_A: 
paulson@18886
  1093
     "\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;  
paulson@18886
  1094
         B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
  1095
         evs \<in> srb \<rbrakk>  
paulson@18886
  1096
      \<Longrightarrow> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, 
paulson@18886
  1097
         Key (sesK(Nb,pairK(A,B))), Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
  1098
apply (erule rev_mp)
paulson@18886
  1099
apply (erule srb.induct)
paulson@18886
  1100
apply (simp_all (no_asm_simp))
paulson@18886
  1101
apply (blast dest: Says_imp_knows_Spy [THEN parts.Inj] Nb_certificate_authentic)
paulson@18886
  1102
done
paulson@18886
  1103
paulson@18886
  1104
paulson@18886
  1105
lemma B_authenticates_A_bis: 
paulson@18886
  1106
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;
paulson@18886
  1107
        Gets B (Cert2) \<in> set evs;  
paulson@18886
  1108
         B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
  1109
         evs \<in> srb \<rbrakk>  
paulson@18886
  1110
      \<Longrightarrow> Outpts (Card A) A  \<lbrace>Agent B, Nonce Nb, Key K, Cert2\<rbrace> \<in> set evs"
paulson@18886
  1111
apply (blast dest: Outpts_B_Card_form_7 B_authenticates_A)
paulson@18886
  1112
done
paulson@18886
  1113
paulson@18886
  1114
paulson@18886
  1115
(*END authentication theorems*)
paulson@18886
  1116
paulson@18886
  1117
paulson@18886
  1118
lemma Confidentiality_A: 
paulson@18886
  1119
      "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
paulson@18886
  1120
                       Key K, Certificate\<rbrace> \<in> set evs;  
paulson@18886
  1121
         Notes Spy \<lbrace>Key K, Nonce Nb, Agent A, Agent B\<rbrace> \<notin> set evs;  
paulson@18886
  1122
         A \<noteq> Spy; B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
  1123
         evs \<in> srb \<rbrakk>           
paulson@18886
  1124
     \<Longrightarrow> Key K \<notin> analz (knows Spy evs)"
paulson@18886
  1125
apply (drule A_authenticates_B)
paulson@18886
  1126
prefer 3
paulson@18886
  1127
apply (erule exE)
paulson@18886
  1128
apply (drule Confidentiality_B)
paulson@18886
  1129
apply auto
paulson@18886
  1130
done
paulson@18886
  1131
paulson@18886
  1132
paulson@18886
  1133
lemma Outpts_imp_knows_agents_secureM_srb: 
paulson@18886
  1134
   "\<lbrakk> Outpts (Card A) A X \<in> set evs; evs \<in> srb \<rbrakk> \<Longrightarrow> X \<in> knows A evs"
paulson@18886
  1135
apply (simp (no_asm_simp) add: Outpts_imp_knows_agents_secureM)
paulson@18886
  1136
done
paulson@18886
  1137
paulson@18886
  1138
paulson@18886
  1139
(*BEGIN key distribution theorems*)
paulson@18886
  1140
lemma A_keydist_to_B: 
paulson@18886
  1141
   "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs;  
paulson@18886
  1142
         \<not>illegalUse(Card B); 
paulson@18886
  1143
         evs \<in> srb \<rbrakk>           
paulson@18886
  1144
     \<Longrightarrow> Key K \<in> analz (knows B evs)"
paulson@18886
  1145
apply (drule A_authenticates_B)
paulson@18886
  1146
prefer 3
paulson@18886
  1147
apply (erule exE)
paulson@18886
  1148
apply (rule Outpts_imp_knows_agents_secureM_srb [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
paulson@18886
  1149
apply assumption+
paulson@18886
  1150
done
paulson@18886
  1151
paulson@18886
  1152
paulson@18886
  1153
lemma B_keydist_to_A: 
paulson@18886
  1154
"\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Cert1, Cert2\<rbrace> \<in> set evs;  
paulson@18886
  1155
   Gets B (Cert2) \<in> set evs;  
paulson@18886
  1156
   B \<noteq> Spy; \<not>illegalUse(Card A); \<not>illegalUse(Card B); 
paulson@18886
  1157
   evs \<in> srb \<rbrakk>  
paulson@18886
  1158
 \<Longrightarrow> Key K \<in> analz (knows A evs)"
paulson@18886
  1159
apply (frule Outpts_B_Card_form_7)
paulson@18886
  1160
apply assumption apply simp
paulson@18886
  1161
apply (frule B_authenticates_A)
paulson@18886
  1162
apply (rule_tac [5] Outpts_imp_knows_agents_secureM_srb [THEN analz.Inj, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
paulson@18886
  1163
apply simp+
paulson@18886
  1164
done
paulson@18886
  1165
paulson@18886
  1166
(*END key distribution theorems*)
paulson@18886
  1167
paulson@18886
  1168
paulson@18886
  1169
paulson@18886
  1170
paulson@18886
  1171
(*BEGIN further theorems about authenticity of verifiers - useful to cards,
paulson@18886
  1172
  and somewhat to agents *)
paulson@18886
  1173
paulson@18886
  1174
(*MSG11
paulson@18886
  1175
If B receives the verifier of msg11, then the verifier originated with msg7.
paulson@18886
  1176
This is clearly not available to B: B can't check the form of the verifier because he doesn't know pairK(A,B)
paulson@18886
  1177
*)
paulson@18886
  1178
lemma Nb_certificate_authentic_B: 
paulson@18886
  1179
     "\<lbrakk> Gets B (Crypt (pairK(A,B)) (Nonce Nb)) \<in> set evs;  
paulson@18886
  1180
        B \<noteq> Spy; \<not>illegalUse(Card B); 
paulson@18886
  1181
        evs \<in> srb \<rbrakk>  
paulson@18886
  1182
     \<Longrightarrow> \<exists> Na. 
paulson@18886
  1183
            Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb,pairK(A,B))),   
paulson@18886
  1184
                Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, 
paulson@18886
  1185
                Crypt (pairK(A,B)) (Nonce Nb)\<rbrace> \<in> set evs"
paulson@18886
  1186
apply (blast dest: Gets_imp_knows_Spy [THEN parts.Inj, THEN Nb_certificate_authentic_bis])
paulson@18886
  1187
done
paulson@18886
  1188
paulson@18886
  1189
(*MSG10
paulson@18886
  1190
If A obtains the verifier of msg10, then the verifier originated with msg7:
paulson@18886
  1191
A_authenticates_B. It is useful to A, who can check the form of the 
paulson@18886
  1192
verifier by application of Outpts_A_Card_form_10.
paulson@18886
  1193
*)
paulson@18886
  1194
paulson@18886
  1195
(*MSG9
paulson@18886
  1196
The first verifier verifies the Pairkey to the card: since it's encrypted
paulson@18886
  1197
under Ka, it must come from the server (if A's card is not cloned).
paulson@18886
  1198
The second verifier verifies both nonces, since it's encrypted under the
paulson@18886
  1199
pairK, it must originate with B's card  (if A and B's cards not cloned).
paulson@18886
  1200
The third verifier verifies Na: since it's encrytped under the card's key,
paulson@18886
  1201
it originated with the card; so the card does not need to save Na
paulson@18886
  1202
in the first place and do a comparison now: it just verifies Na through the
paulson@18886
  1203
verifier. Three theorems related to these three statements.
paulson@18886
  1204
paulson@18886
  1205
Recall that a card can check the form of the verifiers (can decrypt them),
paulson@18886
  1206
while an agent in general cannot, if not provided with a suitable theorem.
paulson@18886
  1207
*)
paulson@18886
  1208
paulson@18886
  1209
(*Card A can't reckon the pairkey - we need to guarantee its integrity!*)
paulson@18886
  1210
lemma Pairkey_certificate_authentic_A_Card: 
paulson@18886
  1211
     "\<lbrakk> Inputs A (Card A)   
paulson@18886
  1212
             \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
paulson@18886
  1213
               Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,  
paulson@18886
  1214
               Cert2, Cert3\<rbrace> \<in> set evs; 
paulson@18886
  1215
         A \<noteq> Spy; Card A \<notin> cloned; evs \<in> srb \<rbrakk>   
paulson@18886
  1216
     \<Longrightarrow> Pk = Pairkey(A,B) \<and>  
paulson@18886
  1217
         Says Server A \<lbrace>Nonce (Pairkey(A,B)),  
paulson@18886
  1218
                  Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>\<rbrace>   
paulson@18886
  1219
           \<in> set evs "
paulson@18886
  1220
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
paulson@18886
  1221
done
paulson@18886
  1222
(*the second conjunct of the thesis might be regarded as a form of integrity 
paulson@18886
  1223
  in the sense of Neuman-Ts'o*)
paulson@18886
  1224
paulson@18886
  1225
lemma Na_Nb_certificate_authentic_A_Card: 
paulson@18886
  1226
      "\<lbrakk> Inputs A (Card A)   
paulson@18886
  1227
             \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
paulson@18886
  1228
          Cert1, Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs; 
paulson@18886
  1229
      A \<noteq> Spy; \<not>illegalUse(Card B); evs \<in> srb \<rbrakk> 
paulson@18886
  1230
   \<Longrightarrow> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key (sesK(Nb, pairK (A, B))),    
paulson@18886
  1231
                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
paulson@18886
  1232
                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
paulson@18886
  1233
           \<in> set evs "
paulson@18886
  1234
apply (frule Inputs_A_Card_9)
paulson@18886
  1235
apply assumption+
paulson@18886
  1236
apply (blast dest: Inputs_A_Card_9 Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd, THEN Na_Nb_certificate_authentic])
paulson@18886
  1237
done
paulson@18886
  1238
paulson@18886
  1239
lemma Na_authentic_A_Card: 
paulson@18886
  1240
     "\<lbrakk> Inputs A (Card A)   
paulson@18886
  1241
             \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
paulson@18886
  1242
                Cert1, Cert2, Cert3\<rbrace> \<in> set evs; 
paulson@18886
  1243
         A \<noteq> Spy; evs \<in> srb \<rbrakk>   
paulson@18886
  1244
     \<Longrightarrow> Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>  
paulson@18886
  1245
           \<in> set evs"
paulson@18886
  1246
apply (blast dest: Inputs_A_Card_9)
paulson@18886
  1247
done
paulson@18886
  1248
paulson@18886
  1249
(* These three theorems for Card A can be put together trivially.
paulson@18886
  1250
They are separated to highlight the different requirements on agents
paulson@18886
  1251
and their cards.*)
paulson@18886
  1252
paulson@18886
  1253
paulson@18886
  1254
lemma Inputs_A_Card_9_authentic: 
paulson@18886
  1255
  "\<lbrakk> Inputs A (Card A)   
paulson@18886
  1256
             \<lbrace>Agent B, Nonce Na, Nonce Nb, Nonce Pk, 
paulson@18886
  1257
               Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>,  
paulson@18886
  1258
               Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>, Cert3\<rbrace> \<in> set evs; 
paulson@18886
  1259
    A \<noteq> Spy; Card A \<notin> cloned; \<not>illegalUse(Card B); evs \<in> srb \<rbrakk>   
paulson@18886
  1260
    \<Longrightarrow>  Says Server A \<lbrace>Nonce Pk, Crypt (shrK A) \<lbrace>Nonce Pk, Agent B\<rbrace>\<rbrace>   
paulson@18886
  1261
           \<in> set evs  \<and> 
paulson@18886
  1262
       Outpts (Card B) B \<lbrace>Nonce Nb, Agent A,  Key (sesK(Nb, pairK (A, B))),    
paulson@18886
  1263
                             Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
paulson@18886
  1264
                             Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
paulson@18886
  1265
           \<in> set evs  \<and> 
paulson@18886
  1266
         Outpts (Card A) A \<lbrace>Nonce Na, Cert3\<rbrace>  
paulson@18886
  1267
           \<in> set evs"
paulson@18886
  1268
apply (blast dest: Inputs_A_Card_9 Na_Nb_certificate_authentic Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Snd] Pairkey_certificate_authentic)
paulson@18886
  1269
done
paulson@18886
  1270
paulson@18886
  1271
paulson@18886
  1272
(*MSG8
paulson@18886
  1273
Nothing to prove because the message is a cleartext that comes from the 
paulson@18886
  1274
network*)
paulson@18886
  1275
paulson@18886
  1276
(*Other messages: nothing to prove because the verifiers involved are new*)
paulson@18886
  1277
paulson@18886
  1278
(*END further theorems about authenticity of verifiers*)
paulson@18886
  1279
paulson@18886
  1280
paulson@18886
  1281
paulson@18886
  1282
(* BEGIN trivial guarantees on outputs for agents *)
paulson@18886
  1283
paulson@18886
  1284
(*MSG4*)
paulson@18886
  1285
lemma SR_U4_imp: 
paulson@18886
  1286
     "\<lbrakk> Outpts (Card A) A \<lbrace>Nonce Na, Crypt (crdK (Card A)) (Nonce Na)\<rbrace> 
paulson@18886
  1287
           \<in> set evs;  
paulson@18886
  1288
         A \<noteq> Spy; evs \<in> srb \<rbrakk>                 
paulson@18886
  1289
     \<Longrightarrow> \<exists> Pk V. Gets A \<lbrace>Pk, V\<rbrace> \<in> set evs"
paulson@18886
  1290
apply (blast dest: Outpts_A_Card_4 Inputs_A_Card_3)
paulson@18886
  1291
done
paulson@18886
  1292
(*weak: could strengthen the model adding verifier for the Pairkey to msg3*)
paulson@18886
  1293
paulson@18886
  1294
paulson@18886
  1295
(*MSG7*)
paulson@18886
  1296
lemma SR_U7_imp: 
paulson@18886
  1297
     "\<lbrakk> Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K,  
paulson@18886
  1298
                      Crypt (pairK(A,B)) \<lbrace>Nonce Na, Nonce Nb\<rbrace>,  
paulson@18886
  1299
                      Cert2\<rbrace> \<in> set evs;  
paulson@18886
  1300
         B \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
  1301
     \<Longrightarrow> Gets B \<lbrace>Agent A, Nonce Na\<rbrace> \<in> set evs"
paulson@18886
  1302
apply (blast dest: Outpts_B_Card_7 Inputs_B_Card_6)
paulson@18886
  1303
done
paulson@18886
  1304
paulson@18886
  1305
(*MSG10*)
paulson@18886
  1306
lemma SR_U10_imp: 
paulson@18886
  1307
     "\<lbrakk> Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, 
paulson@18886
  1308
                           Key K, Crypt (pairK(A,B)) (Nonce Nb)\<rbrace>  
paulson@18886
  1309
         \<in> set evs;  
paulson@18886
  1310
        A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
  1311
     \<Longrightarrow> \<exists> Cert1 Cert2.  
paulson@18886
  1312
                   Gets A \<lbrace>Nonce (Pairkey (A, B)), Cert1\<rbrace> \<in> set evs \<and>  
paulson@18886
  1313
                   Gets A \<lbrace>Nonce Nb, Cert2\<rbrace> \<in> set evs"
paulson@18886
  1314
apply (blast dest: Outpts_A_Card_10 Inputs_A_Card_9)
paulson@18886
  1315
done
paulson@18886
  1316
paulson@18886
  1317
paulson@18886
  1318
(*END trivial guarantees on outputs for agents*)
paulson@18886
  1319
paulson@18886
  1320
paulson@18886
  1321
paulson@18886
  1322
(*INTEGRITY*)
paulson@18886
  1323
lemma Outpts_Server_not_evs: 
paulson@18886
  1324
      "evs \<in> srb \<Longrightarrow> Outpts (Card Server) P X \<notin> set evs"
paulson@18886
  1325
apply (erule srb.induct)
paulson@18886
  1326
apply auto
paulson@18886
  1327
done
paulson@18886
  1328
paulson@18886
  1329
text{*@{term step2_integrity} also is a reliability theorem*}
paulson@18886
  1330
lemma Says_Server_message_form: 
paulson@18886
  1331
     "\<lbrakk> Says Server A \<lbrace>Pk, Certificate\<rbrace> \<in> set evs;  
paulson@18886
  1332
         evs \<in> srb \<rbrakk>                   
paulson@18886
  1333
     \<Longrightarrow> \<exists> B. Pk = Nonce (Pairkey(A,B)) \<and>  
paulson@18886
  1334
         Certificate = Crypt (shrK A) \<lbrace>Nonce (Pairkey(A,B)), Agent B\<rbrace>"
paulson@18886
  1335
apply (erule rev_mp)
paulson@18886
  1336
apply (erule srb.induct)
paulson@18886
  1337
apply auto
paulson@18886
  1338
apply (blast dest!: Outpts_Server_not_evs)+
paulson@18886
  1339
done
paulson@18886
  1340
(*cannot be made useful to A in form of a Gets event*)
paulson@18886
  1341
paulson@18886
  1342
text{*
paulson@18886
  1343
  step4integrity is @{term Outpts_A_Card_form_4}
paulson@18886
  1344
paulson@18886
  1345
  step7integrity is @{term Outpts_B_Card_form_7}
paulson@18886
  1346
*}
paulson@18886
  1347
paulson@18886
  1348
lemma step8_integrity: 
paulson@18886
  1349
     "\<lbrakk> Says B A \<lbrace>Nonce Nb, Certificate\<rbrace> \<in> set evs;  
paulson@18886
  1350
         B \<noteq> Server; B \<noteq> Spy; evs \<in> srb \<rbrakk>                   
paulson@18886
  1351
     \<Longrightarrow> \<exists> Cert2 K.   
paulson@18886
  1352
    Outpts (Card B) B \<lbrace>Nonce Nb, Agent A, Key K, Certificate, Cert2\<rbrace> \<in> set evs"
paulson@18886
  1353
apply (erule rev_mp)
paulson@18886
  1354
apply (erule srb.induct)
paulson@18886
  1355
prefer 18 apply (fastsimp dest: Outpts_A_Card_form_10)
paulson@18886
  1356
apply auto
paulson@18886
  1357
done
paulson@18886
  1358
paulson@18886
  1359
paulson@18886
  1360
text{*  step9integrity is @{term Inputs_A_Card_form_9}
paulson@18886
  1361
        step10integrity is @{term Outpts_A_Card_form_10}.
paulson@18886
  1362
*}
paulson@18886
  1363
paulson@18886
  1364
paulson@18886
  1365
lemma step11_integrity: 
paulson@18886
  1366
     "\<lbrakk> Says A B (Certificate) \<in> set evs; 
paulson@18886
  1367
         \<forall> p q. Certificate \<noteq> \<lbrace>p, q\<rbrace>;  
paulson@18886
  1368
         A \<noteq> Spy; evs \<in> srb \<rbrakk>  
paulson@18886
  1369
     \<Longrightarrow> \<exists> K Nb.  
paulson@18886
  1370
      Outpts (Card A) A \<lbrace>Agent B, Nonce Nb, Key K, Certificate\<rbrace> \<in> set evs"
paulson@18886
  1371
apply (erule rev_mp)
paulson@18886
  1372
apply (erule srb.induct)
paulson@18886
  1373
apply auto
paulson@18886
  1374
done
paulson@18886
  1375
paulson@18886
  1376
end
paulson@18886
  1377