1(* Title: HOL/Auth/ZhouGollmann.thy 2 Author: Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab 3 Copyright 2003 University of Cambridge 4 5The protocol of 6 Jianying Zhou and Dieter Gollmann, 7 A Fair Non-Repudiation Protocol, 8 Security and Privacy 1996 (Oakland) 9 55-61 10*) 11 12theory ZhouGollmann imports Public begin 13 14abbreviation 15 TTP :: agent where "TTP == Server" 16 17abbreviation f_sub :: nat where "f_sub == 5" 18abbreviation f_nro :: nat where "f_nro == 2" 19abbreviation f_nrr :: nat where "f_nrr == 3" 20abbreviation f_con :: nat where "f_con == 4" 21 22 23definition broken :: "agent set" where 24 \<comment> \<open>the compromised honest agents; TTP is included as it's not allowed to 25 use the protocol\<close> 26 "broken == bad - {Spy}" 27 28declare broken_def [simp] 29 30inductive_set zg :: "event list set" 31 where 32 33 Nil: "[] \<in> zg" 34 35| Fake: "[| evsf \<in> zg; X \<in> synth (analz (spies evsf)) |] 36 ==> Says Spy B X # evsf \<in> zg" 37 38| Reception: "[| evsr \<in> zg; Says A B X \<in> set evsr |] ==> Gets B X # evsr \<in> zg" 39 40 (*L is fresh for honest agents. 41 We don't require K to be fresh because we don't bother to prove secrecy! 42 We just assume that the protocol's objective is to deliver K fairly, 43 rather than to keep M secret.*) 44| ZG1: "[| evs1 \<in> zg; Nonce L \<notin> used evs1; C = Crypt K (Number m); 45 K \<in> symKeys; 46 NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>|] 47 ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> # evs1 \<in> zg" 48 49 (*B must check that NRO is A's signature to learn the sender's name*) 50| ZG2: "[| evs2 \<in> zg; 51 Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs2; 52 NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>; 53 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>|] 54 ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> # evs2 \<in> zg" 55 56 (*A must check that NRR is B's signature to learn the sender's name; 57 without spy, the matching label would be enough*) 58| ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys; 59 Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs3; 60 Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs3; 61 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>; 62 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>|] 63 ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> 64 # evs3 \<in> zg" 65 66 (*TTP checks that sub_K is A's signature to learn who issued K, then 67 gives credentials to A and B. The Notes event models the availability of 68 the credentials, but the act of fetching them is not modelled. We also 69 give con_K to the Spy. This makes the threat model more dangerous, while 70 also allowing lemma @{text Crypt_used_imp_spies} to omit the condition 71 @{term "K \<noteq> priK TTP"}. *) 72| ZG4: "[| evs4 \<in> zg; K \<in> symKeys; 73 Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> 74 \<in> set evs4; 75 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 76 con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, 77 Nonce L, Key K\<rbrace>|] 78 ==> Says TTP Spy con_K 79 # 80 Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> 81 # evs4 \<in> zg" 82 83 84declare Says_imp_knows_Spy [THEN analz.Inj, dest] 85declare Fake_parts_insert_in_Un [dest] 86declare analz_into_parts [dest] 87 88declare symKey_neq_priEK [simp] 89declare symKey_neq_priEK [THEN not_sym, simp] 90 91 92text\<open>A "possibility property": there are traces that reach the end\<close> 93lemma "[|A \<noteq> B; TTP \<noteq> A; TTP \<noteq> B; K \<in> symKeys|] ==> 94 \<exists>L. \<exists>evs \<in> zg. 95 Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, 96 Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace> 97 \<in> set evs" 98apply (intro exI bexI) 99apply (rule_tac [2] zg.Nil 100 [THEN zg.ZG1, THEN zg.Reception [of _ A B], 101 THEN zg.ZG2, THEN zg.Reception [of _ B A], 102 THEN zg.ZG3, THEN zg.Reception [of _ A TTP], 103 THEN zg.ZG4]) 104apply (basic_possibility, auto) 105done 106 107subsection \<open>Basic Lemmas\<close> 108 109lemma Gets_imp_Says: 110 "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs" 111apply (erule rev_mp) 112apply (erule zg.induct, auto) 113done 114 115lemma Gets_imp_knows_Spy: 116 "[| Gets B X \<in> set evs; evs \<in> zg |] ==> X \<in> spies evs" 117by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 118 119 120text\<open>Lets us replace proofs about \<^term>\<open>used evs\<close> by simpler proofs 121about \<^term>\<open>parts (spies evs)\<close>.\<close> 122lemma Crypt_used_imp_spies: 123 "[| Crypt K X \<in> used evs; evs \<in> zg |] 124 ==> Crypt K X \<in> parts (spies evs)" 125apply (erule rev_mp) 126apply (erule zg.induct) 127apply (simp_all add: parts_insert_knows_A) 128done 129 130lemma Notes_TTP_imp_Gets: 131 "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> 132 \<in> set evs; 133 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 134 evs \<in> zg|] 135 ==> Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" 136apply (erule rev_mp) 137apply (erule zg.induct, auto) 138done 139 140text\<open>For reasoning about C, which is encrypted in message ZG2\<close> 141lemma ZG2_msg_in_parts_spies: 142 "[|Gets B \<lbrace>F, B', L, C, X\<rbrace> \<in> set evs; evs \<in> zg|] 143 ==> C \<in> parts (spies evs)" 144by (blast dest: Gets_imp_Says) 145 146(*classical regularity lemma on priK*) 147lemma Spy_see_priK [simp]: 148 "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)" 149apply (erule zg.induct) 150apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 151done 152 153text\<open>So that blast can use it too\<close> 154declare Spy_see_priK [THEN [2] rev_iffD1, dest!] 155 156lemma Spy_analz_priK [simp]: 157 "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)" 158by auto 159 160 161subsection\<open>About NRO: Validity for \<^term>\<open>B\<close>\<close> 162 163text\<open>Below we prove that if \<^term>\<open>NRO\<close> exists then \<^term>\<open>A\<close> definitely 164sent it, provided \<^term>\<open>A\<close> is not broken.\<close> 165 166text\<open>Strong conclusion for a good agent\<close> 167lemma NRO_validity_good: 168 "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>; 169 NRO \<in> parts (spies evs); 170 A \<notin> bad; evs \<in> zg |] 171 ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs" 172apply clarify 173apply (erule rev_mp) 174apply (erule zg.induct) 175apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 176done 177 178lemma NRO_sender: 179 "[|Says A' B \<lbrace>n, b, l, C, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|] 180 ==> A' \<in> {A,Spy}" 181apply (erule rev_mp) 182apply (erule zg.induct, simp_all) 183done 184 185text\<open>Holds also for \<^term>\<open>A = Spy\<close>!\<close> 186theorem NRO_validity: 187 "[|Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs; 188 NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>; 189 A \<notin> broken; evs \<in> zg |] 190 ==> Says A B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs" 191apply (drule Gets_imp_Says, assumption) 192apply clarify 193apply (frule NRO_sender, auto) 194txt\<open>We are left with the case where the sender is \<^term>\<open>Spy\<close> and not 195 equal to \<^term>\<open>A\<close>, because \<^term>\<open>A \<notin> bad\<close>. 196 Thus theorem \<open>NRO_validity_good\<close> applies.\<close> 197apply (blast dest: NRO_validity_good [OF refl]) 198done 199 200 201subsection\<open>About NRR: Validity for \<^term>\<open>A\<close>\<close> 202 203text\<open>Below we prove that if \<^term>\<open>NRR\<close> exists then \<^term>\<open>B\<close> definitely 204sent it, provided \<^term>\<open>B\<close> is not broken.\<close> 205 206text\<open>Strong conclusion for a good agent\<close> 207lemma NRR_validity_good: 208 "[|NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>; 209 NRR \<in> parts (spies evs); 210 B \<notin> bad; evs \<in> zg |] 211 ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" 212apply clarify 213apply (erule rev_mp) 214apply (erule zg.induct) 215apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 216done 217 218lemma NRR_sender: 219 "[|Says B' A \<lbrace>n, a, l, Crypt (priK B) X\<rbrace> \<in> set evs; evs \<in> zg|] 220 ==> B' \<in> {B,Spy}" 221apply (erule rev_mp) 222apply (erule zg.induct, simp_all) 223done 224 225text\<open>Holds also for \<^term>\<open>B = Spy\<close>!\<close> 226theorem NRR_validity: 227 "[|Says B' A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs; 228 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>; 229 B \<notin> broken; evs \<in> zg|] 230 ==> Says B A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" 231apply clarify 232apply (frule NRR_sender, auto) 233txt\<open>We are left with the case where \<^term>\<open>B' = Spy\<close> and \<^term>\<open>B' \<noteq> B\<close>, 234 i.e. \<^term>\<open>B \<notin> bad\<close>, when we can apply \<open>NRR_validity_good\<close>.\<close> 235 apply (blast dest: NRR_validity_good [OF refl]) 236done 237 238 239subsection\<open>Proofs About \<^term>\<open>sub_K\<close>\<close> 240 241text\<open>Below we prove that if \<^term>\<open>sub_K\<close> exists then \<^term>\<open>A\<close> definitely 242sent it, provided \<^term>\<open>A\<close> is not broken.\<close> 243 244text\<open>Strong conclusion for a good agent\<close> 245lemma sub_K_validity_good: 246 "[|sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 247 sub_K \<in> parts (spies evs); 248 A \<notin> bad; evs \<in> zg |] 249 ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" 250apply clarify 251apply (erule rev_mp) 252apply (erule zg.induct) 253apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 254txt\<open>Fake\<close> 255apply (blast dest!: Fake_parts_sing_imp_Un) 256done 257 258lemma sub_K_sender: 259 "[|Says A' TTP \<lbrace>n, b, l, k, Crypt (priK A) X\<rbrace> \<in> set evs; evs \<in> zg|] 260 ==> A' \<in> {A,Spy}" 261apply (erule rev_mp) 262apply (erule zg.induct, simp_all) 263done 264 265text\<open>Holds also for \<^term>\<open>A = Spy\<close>!\<close> 266theorem sub_K_validity: 267 "[|Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs; 268 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 269 A \<notin> broken; evs \<in> zg |] 270 ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" 271apply (drule Gets_imp_Says, assumption) 272apply clarify 273apply (frule sub_K_sender, auto) 274txt\<open>We are left with the case where the sender is \<^term>\<open>Spy\<close> and not 275 equal to \<^term>\<open>A\<close>, because \<^term>\<open>A \<notin> bad\<close>. 276 Thus theorem \<open>sub_K_validity_good\<close> applies.\<close> 277apply (blast dest: sub_K_validity_good [OF refl]) 278done 279 280 281 282subsection\<open>Proofs About \<^term>\<open>con_K\<close>\<close> 283 284text\<open>Below we prove that if \<^term>\<open>con_K\<close> exists, then \<^term>\<open>TTP\<close> has it, 285and therefore \<^term>\<open>A\<close> and \<^term>\<open>B\<close>) can get it too. Moreover, we know 286that \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>\<close> 287 288lemma con_K_validity: 289 "[|con_K \<in> used evs; 290 con_K = Crypt (priK TTP) 291 \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>; 292 evs \<in> zg |] 293 ==> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> 294 \<in> set evs" 295apply clarify 296apply (erule rev_mp) 297apply (erule zg.induct) 298apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 299txt\<open>Fake\<close> 300apply (blast dest!: Fake_parts_sing_imp_Un) 301txt\<open>ZG2\<close> 302apply (blast dest: parts_cut) 303done 304 305text\<open>If \<^term>\<open>TTP\<close> holds \<^term>\<open>con_K\<close> then \<^term>\<open>A\<close> sent 306 \<^term>\<open>sub_K\<close>. We assume that \<^term>\<open>A\<close> is not broken. Importantly, nothing 307 needs to be assumed about the form of \<^term>\<open>con_K\<close>!\<close> 308lemma Notes_TTP_imp_Says_A: 309 "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> 310 \<in> set evs; 311 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 312 A \<notin> broken; evs \<in> zg|] 313 ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" 314apply clarify 315apply (erule rev_mp) 316apply (erule zg.induct) 317apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 318txt\<open>ZG4\<close> 319apply clarify 320apply (rule sub_K_validity, auto) 321done 322 323text\<open>If \<^term>\<open>con_K\<close> exists, then \<^term>\<open>A\<close> sent \<^term>\<open>sub_K\<close>. We again 324 assume that \<^term>\<open>A\<close> is not broken.\<close> 325theorem B_sub_K_validity: 326 "[|con_K \<in> used evs; 327 con_K = Crypt (priK TTP) \<lbrace>Number f_con, Agent A, Agent B, 328 Nonce L, Key K\<rbrace>; 329 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 330 A \<notin> broken; evs \<in> zg|] 331 ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs" 332by (blast dest: con_K_validity Notes_TTP_imp_Says_A) 333 334 335subsection\<open>Proving fairness\<close> 336 337text\<open>Cannot prove that, if \<^term>\<open>B\<close> has NRO, then \<^term>\<open>A\<close> has her NRR. 338It would appear that \<^term>\<open>B\<close> has a small advantage, though it is 339useless to win disputes: \<^term>\<open>B\<close> needs to present \<^term>\<open>con_K\<close> as well.\<close> 340 341text\<open>Strange: unicity of the label protects \<^term>\<open>A\<close>?\<close> 342lemma A_unicity: 343 "[|NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>; 344 NRO \<in> parts (spies evs); 345 Says A B \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M', NRO'\<rbrace> 346 \<in> set evs; 347 A \<notin> bad; evs \<in> zg |] 348 ==> M'=M" 349apply clarify 350apply (erule rev_mp) 351apply (erule rev_mp) 352apply (erule zg.induct) 353apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 354txt\<open>ZG1: freshness\<close> 355apply (blast dest: parts.Body) 356done 357 358 359text\<open>Fairness lemma: if \<^term>\<open>sub_K\<close> exists, then \<^term>\<open>A\<close> holds 360NRR. Relies on unicity of labels.\<close> 361lemma sub_K_implies_NRR: 362 "[| NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>; 363 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>; 364 sub_K \<in> parts (spies evs); 365 NRO \<in> parts (spies evs); 366 sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; 367 A \<notin> bad; evs \<in> zg |] 368 ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" 369apply clarify 370apply hypsubst_thin 371apply (erule rev_mp) 372apply (erule rev_mp) 373apply (erule zg.induct) 374apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 375txt\<open>Fake\<close> 376apply blast 377txt\<open>ZG1: freshness\<close> 378apply (blast dest: parts.Body) 379txt\<open>ZG3\<close> 380apply (blast dest: A_unicity [OF refl]) 381done 382 383 384lemma Crypt_used_imp_L_used: 385 "[| Crypt (priK TTP) \<lbrace>F, A, B, L, K\<rbrace> \<in> used evs; evs \<in> zg |] 386 ==> L \<in> used evs" 387apply (erule rev_mp) 388apply (erule zg.induct, auto) 389txt\<open>Fake\<close> 390apply (blast dest!: Fake_parts_sing_imp_Un) 391txt\<open>ZG2: freshness\<close> 392apply (blast dest: parts.Body) 393done 394 395 396text\<open>Fairness for \<^term>\<open>A\<close>: if \<^term>\<open>con_K\<close> and \<^term>\<open>NRO\<close> exist, 397then \<^term>\<open>A\<close> holds NRR. \<^term>\<open>A\<close> must be uncompromised, but there is no 398assumption about \<^term>\<open>B\<close>.\<close> 399theorem A_fairness_NRO: 400 "[|con_K \<in> used evs; 401 NRO \<in> parts (spies evs); 402 con_K = Crypt (priK TTP) 403 \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>; 404 NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, Crypt K M\<rbrace>; 405 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, Crypt K M\<rbrace>; 406 A \<notin> bad; evs \<in> zg |] 407 ==> Gets A \<lbrace>Number f_nrr, Agent A, Nonce L, NRR\<rbrace> \<in> set evs" 408apply clarify 409apply (erule rev_mp) 410apply (erule rev_mp) 411apply (erule zg.induct) 412apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 413 txt\<open>Fake\<close> 414 apply (simp add: parts_insert_knows_A) 415 apply (blast dest: Fake_parts_sing_imp_Un) 416 txt\<open>ZG1\<close> 417 apply (blast dest: Crypt_used_imp_L_used) 418 txt\<open>ZG2\<close> 419 apply (blast dest: parts_cut) 420txt\<open>ZG4\<close> 421apply (blast intro: sub_K_implies_NRR [OF refl] 422 dest: Gets_imp_knows_Spy [THEN parts.Inj]) 423done 424 425text\<open>Fairness for \<^term>\<open>B\<close>: NRR exists at all, then \<^term>\<open>B\<close> holds NRO. 426\<^term>\<open>B\<close> must be uncompromised, but there is no assumption about \<^term>\<open>A\<close>.\<close> 427theorem B_fairness_NRR: 428 "[|NRR \<in> used evs; 429 NRR = Crypt (priK B) \<lbrace>Number f_nrr, Agent A, Nonce L, C\<rbrace>; 430 NRO = Crypt (priK A) \<lbrace>Number f_nro, Agent B, Nonce L, C\<rbrace>; 431 B \<notin> bad; evs \<in> zg |] 432 ==> Gets B \<lbrace>Number f_nro, Agent B, Nonce L, C, NRO\<rbrace> \<in> set evs" 433apply clarify 434apply (erule rev_mp) 435apply (erule zg.induct) 436apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all) 437txt\<open>Fake\<close> 438apply (blast dest!: Fake_parts_sing_imp_Un) 439txt\<open>ZG2\<close> 440apply (blast dest: parts_cut) 441done 442 443 444text\<open>If \<^term>\<open>con_K\<close> exists at all, then \<^term>\<open>B\<close> can get it, by \<open>con_K_validity\<close>. Cannot conclude that also NRO is available to \<^term>\<open>B\<close>, 445because if \<^term>\<open>A\<close> were unfair, \<^term>\<open>A\<close> could build message 3 without 446building message 1, which contains NRO.\<close> 447 448end 449