src/HOL/UNITY/Simple/NSP_Bad.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Mon Mar 05 15:47:11 2001 +0100
@@ -0,0 +1,59 @@
+(*  Title:      HOL/Auth/NSP_Bad
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+add_path "../Auth"; use_thy"NSP_Bad";
+
+Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
+
+Original file is ../Auth/NS_Public_Bad
+*)
+
+NSP_Bad = Public + Constrains + 
+
+types state = event list
+
+constdefs
+  
+  (*The spy MAY say anything he CAN say.  We do not expect him to
+    invent new nonces here, but he can also use NS1.  Common to
+    all similar protocols.*)
+  Fake :: "(state*state) set"
+    "Fake == {(s,s').
+	      EX B X. s' = Says Spy B X # s
+		    & X: synth (analz (spies s))}"
+  
+  (*The numeric suffixes on A identify the rule*)
+
+  (*Alice initiates a protocol run, sending a nonce to Bob*)
+  NS1 :: "(state*state) set"
+    "NS1 == {(s1,s').
+	     EX A1 B NA.
+	         s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
+	       & Nonce NA ~: used s1}"
+  
+  (*Bob responds to Alice's message with a further nonce*)
+  NS2 :: "(state*state) set"
+    "NS2 == {(s2,s').
+	     EX A' A2 B NA NB.
+	         s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
+               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
+	       & Nonce NB ~: used s2}"
+ 
+  (*Alice proves her existence by sending NB back to Bob.*)
+  NS3 :: "(state*state) set"
+    "NS3 == {(s3,s').
+	     EX A3 B' B NA NB.
+	         s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
+               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
+	       & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
+
+
+
+constdefs
+  Nprg :: state program
+    (*Initial trace is empty*)
+    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
+
+end