--- a/src/HOL/Auth/NS_Public.ML Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Thu Jan 09 10:22:11 1997 +0100
@@ -28,7 +28,8 @@
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
+ addss (!simpset setsolver safe_solver))));
result();
@@ -82,24 +83,6 @@
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!i. evs : ns_public ==> \
-\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
@@ -117,11 +100,9 @@
\ Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (sees lost Spy evs)";
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSEs partsEs
- addEs [nonce_not_seen_now]) 4);
+by (fast_tac (!claset addSEs partsEs) 4);
(*NS2*)
-by (fast_tac (!claset addSEs partsEs
- addEs [nonce_not_seen_now]) 3);
+by (fast_tac (!claset addSEs partsEs) 3);
(*Fake*)
by (best_tac (!claset addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
@@ -141,12 +122,13 @@
\ A=A' & B=B')";
by (analz_induct_tac 1);
(*NS1*)
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
+ REPEAT (fast_tac (!claset addSEs partsEs) 3));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
@@ -176,16 +158,16 @@
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+by (spy_analz_tac 1);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+(*14 seconds. Much slower still if one tries to prove all NS2 in one step.*)
+by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
addDs [unique_NA]) 1);
bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
@@ -203,8 +185,7 @@
by (ALLGOALS Asm_simp_tac);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
@@ -261,12 +242,13 @@
\ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B')";
by (analz_induct_tac 1);
(*NS2*)
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
+ REPEAT (fast_tac (!claset addSEs partsEs) 3));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
@@ -299,17 +281,16 @@
addDs [unique_NB]) 4);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+by (spy_analz_tac 1);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 3);
+by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 2);
+by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp));
@@ -330,8 +311,7 @@
by (ALLGOALS Asm_simp_tac);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
@@ -377,8 +357,7 @@
(*Fake, NS2, NS3*)
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
--- a/src/HOL/Auth/NS_Public.thy Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/NS_Public.thy Thu Jan 09 10:22:11 1997 +0100
@@ -24,16 +24,15 @@
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs: ns_public; A ~= B |]
- ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
+ NS1 "[| evs: ns_public; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
# evs : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs: ns_public; A ~= B;
+ NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs)),
- Agent B|})
+ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})
# evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
--- a/src/HOL/Auth/NS_Public_Bad.ML Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Jan 09 10:22:11 1997 +0100
@@ -32,7 +32,8 @@
by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2);
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver)));
by (REPEAT_FIRST (resolve_tac [refl, conjI]));
-by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver))));
+by (REPEAT_FIRST (fast_tac (!claset addSEs [Nonce_supply RS notE]
+ addss (!simpset setsolver safe_solver))));
result();
@@ -86,24 +87,6 @@
AddSDs [Spy_see_priK_D, Spy_analz_priK_D];
-(*** Future nonces can't be seen or used! ***)
-
-goal thy "!!i. evs : ns_public ==> \
-\ length evs <= i --> Nonce (newN i) ~: parts (sees lost Spy evs)";
-by (parts_induct_tac 1);
-by (REPEAT_FIRST (fast_tac (!claset
- addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [leD RS notE]
- addDs [impOfSubs analz_subset_parts,
- impOfSubs parts_insert_subset_Un,
- Suc_leD]
- addss (!simpset))));
-qed_spec_mp "new_nonces_not_seen";
-Addsimps [new_nonces_not_seen];
-
-val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
-
fun analz_induct_tac i =
etac ns_public.induct i THEN
ALLGOALS (asm_simp_tac
@@ -122,11 +105,9 @@
\ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)";
by (analz_induct_tac 1);
(*NS3*)
-by (fast_tac (!claset addSEs partsEs
- addEs [nonce_not_seen_now]) 4);
+by (fast_tac (!claset addSEs partsEs) 4);
(*NS2*)
-by (fast_tac (!claset addSEs partsEs
- addEs [nonce_not_seen_now]) 3);
+by (fast_tac (!claset addSEs partsEs) 3);
(*Fake*)
by (best_tac (!claset addIs [analz_insertI]
addDs [impOfSubs analz_subset_parts,
@@ -146,12 +127,13 @@
\ A=A' & B=B')";
by (analz_induct_tac 1);
(*NS1*)
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NA = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
+ REPEAT (fast_tac (!claset addSEs partsEs) 3));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
@@ -181,15 +163,14 @@
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addIs [impOfSubs analz_subset_parts]) 2);
(*Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+by (spy_analz_tac 1);
(*NS2*)
by (Step_tac 1);
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
addDs [unique_NA]) 1);
bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp));
@@ -206,8 +187,7 @@
by (ALLGOALS Asm_simp_tac);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
@@ -219,7 +199,8 @@
(*NS2*)
by (Step_tac 1);
by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1));
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+(*11 seconds*)
+by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
addDs [unique_NA]) 1);
qed_spec_mp "NA_decrypt_imp_B_msg";
@@ -266,12 +247,13 @@
\ A=A' & NA=NA')";
by (analz_induct_tac 1);
(*NS2*)
+by (simp_tac (!simpset addsimps [all_conj_distrib]) 3);
by (expand_case_tac "NB = ?y" 3 THEN
- REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3));
+ REPEAT (fast_tac (!claset addSEs partsEs) 3));
(*Base*)
by (fast_tac (!claset addss (!simpset)) 1);
(*Fake*)
-by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1);
+by (simp_tac (!simpset addsimps [all_conj_distrib, parts_insert_sees]) 1);
by (step_tac (!claset addSIs [analz_insertI]) 1);
by (ex_strip_tac 1);
by (best_tac (!claset delrules [conjI]
@@ -299,26 +281,18 @@
by (analz_induct_tac 1);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+by (spy_analz_tac 1);
(*NS2 and NS3*)
by (Step_tac 1);
+by (TRYALL (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI])));
(*NS2*)
-by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
- addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 3);
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
-by (Fast_tac 1);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
+by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
+ addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
(*NS3*)
-by (Fast_tac 2);
-by (fast_tac (!claset addSEs partsEs
- addSDs [Says_imp_sees_Spy' RS parts.Inj,
- new_nonces_not_seen,
- impOfSubs analz_subset_parts]) 1);
-
by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1
THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1));
by (Fast_tac 1);
@@ -338,8 +312,7 @@
by (ALLGOALS Asm_simp_tac);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
by (REPEAT_FIRST (resolve_tac [impI, conjI]));
by (fast_tac (!claset addss (!simpset)) 1);
@@ -380,16 +353,15 @@
by (analz_induct_tac 1);
(*NS1*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
(*Fake*)
-by (REPEAT_FIRST spy_analz_tac);
+by (spy_analz_tac 1);
(*NS2 and NS3*)
by (Step_tac 1);
+by (fast_tac (!claset addSIs [impOfSubs analz_subset_parts, usedI]) 1);
(*NS2*)
by (fast_tac (!claset addSEs partsEs
- addSDs [new_nonces_not_seen,
- Says_imp_sees_Spy' RS parts.Inj]) 2);
+ addSDs [Says_imp_sees_Spy' RS parts.Inj]) 2);
by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj]
addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1);
(*NS3*)
--- a/src/HOL/Auth/NS_Public_Bad.thy Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Jan 09 10:22:11 1997 +0100
@@ -28,15 +28,15 @@
==> Says Spy B X # evs : ns_public"
(*Alice initiates a protocol run, sending a nonce to Bob*)
- NS1 "[| evs: ns_public; A ~= B |]
- ==> Says A B (Crypt (pubK B) {|Nonce (newN(length evs)), Agent A|})
+ NS1 "[| evs: ns_public; A ~= B; Nonce NA ~: used evs |]
+ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})
# evs : ns_public"
(*Bob responds to Alice's message with a further nonce*)
- NS2 "[| evs: ns_public; A ~= B;
+ NS2 "[| evs: ns_public; A ~= B; Nonce NB ~: used evs;
Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})
: set_of_list evs |]
- ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN(length evs))|})
+ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|})
# evs : ns_public"
(*Alice proves her existence by sending NB back to Bob.*)
--- a/src/HOL/Auth/Public.ML Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/Public.ML Thu Jan 09 10:22:11 1997 +0100
@@ -11,6 +11,9 @@
open Public;
+(*Injectiveness of new nonces*)
+AddIffs [inj_newN RS inj_eq];
+
(*Holds because Friend is injective: thus cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
by (Auto_tac());
@@ -24,23 +27,6 @@
will not!*)
Addsimps [o_def];
-(*** Basic properties of pubK ***)
-
-(*Injectiveness and freshness of new keys and nonces*)
-AddIffs [inj_pubK RS inj_eq, inj_newN RS inj_eq];
-
-(** Rewrites should not refer to initState(Friend i)
- -- not in normal form! **)
-
-Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
-
-goal thy "Nonce (newN i) ~: parts (initState lost B)";
-by (agent.induct_tac "B" 1);
-by (Auto_tac ());
-qed "newN_notin_initState";
-
-AddIffs [newN_notin_initState];
-
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
by (agent.induct_tac "C" 1);
by (auto_tac (!claset addIs [range_eqI], !simpset));
@@ -63,6 +49,11 @@
by (Auto_tac ());
qed "sees_mono";
+(*** Basic properties of pubK & priK ***)
+
+AddIffs [inj_pubK RS inj_eq];
+Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
+
(*Agents see their own private keys!*)
goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
by (list.induct_tac "evs" 1);
@@ -157,6 +148,48 @@
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
+(*** Fresh nonces ***)
+
+goal thy "Nonce N ~: parts (initState lost B)";
+by (agent.induct_tac "B" 1);
+by (Auto_tac ());
+qed "Nonce_notin_initState";
+
+AddIffs [Nonce_notin_initState];
+
+goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
+be (impOfSubs parts_mono) 1;
+by (Fast_tac 1);
+qed "usedI";
+
+AddIs [usedI];
+
+(*Yields a supply of fresh nonces for possibility theorems.*)
+goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
+by (list.induct_tac "evs" 1);
+by (res_inst_tac [("x","0")] exI 1);
+by (Step_tac 1);
+by (Full_simp_tac 1);
+by (event.induct_tac "a" 1);
+by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
+by (msg.induct_tac "msg" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
+by (Step_tac 1);
+(*MPair case*)
+by (res_inst_tac [("x","Na+Nb")] exI 2);
+by (fast_tac (!claset addSEs [add_leE]) 2);
+(*Nonce case*)
+by (res_inst_tac [("x","N + Suc nat")] exI 1);
+by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
+val lemma = result();
+
+goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
+br (lemma RS exE) 1;
+br selectI 1;
+by (Fast_tac 1);
+qed "Nonce_supply";
+
+
(** Power of the Spy **)
(*The Spy can see more than anybody else, except for their initial state*)
--- a/src/HOL/Auth/Public.thy Thu Jan 09 10:20:03 1997 +0100
+++ b/src/HOL/Auth/Public.thy Thu Jan 09 10:22:11 1997 +0100
@@ -50,6 +50,13 @@
sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs"
+constdefs
+ (*Set of items that might be visible to somebody: complement of the set
+ of fresh items*)
+ used :: event list => msg set
+ "used evs == parts (UN lost B. sees lost B evs)"
+
+
(*Agents generate "random" nonces, uniquely determined by their argument.*)
consts
newN :: nat => nat