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