# HG changeset patch # User paulson # Date 852801731 -3600 # Node ID 47de509bdd55432b1a89ab7081d879704972cf2f # Parent 40efb87985b50fcf78e725e0c740b815e13a05a6 New treatment of nonce creation diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/NS_Public.ML --- 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); diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/NS_Public.thy --- 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.*) diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/NS_Public_Bad.ML --- 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*) diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/NS_Public_Bad.thy --- 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.*) diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/Public.ML --- 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*) diff -r 40efb87985b5 -r 47de509bdd55 src/HOL/Auth/Public.thy --- 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