src/HOL/UNITY/Simple/NSP_Bad.thy
author paulson
Sat Feb 08 16:05:33 2003 +0100 (2003-02-08)
changeset 13812 91713a1915ee
parent 13797 baefae13ad37
child 14203 97df98601d23
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
paulson@11195
     1
(*  Title:      HOL/Auth/NSP_Bad
paulson@11195
     2
    ID:         $Id$
paulson@11195
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11195
     4
    Copyright   1996  University of Cambridge
paulson@11195
     5
paulson@11195
     6
add_path "../Auth"; use_thy"NSP_Bad";
paulson@11195
     7
paulson@11195
     8
Security protocols in UNITY: Needham-Schroeder, public keys (flawed version).
paulson@11195
     9
paulson@11195
    10
Original file is ../Auth/NS_Public_Bad
paulson@11195
    11
*)
paulson@11195
    12
paulson@13797
    13
NSP_Bad = Public + UNITY_Main + 
paulson@11195
    14
paulson@11195
    15
types state = event list
paulson@11195
    16
paulson@11195
    17
constdefs
paulson@11195
    18
  
paulson@11195
    19
  (*The spy MAY say anything he CAN say.  We do not expect him to
paulson@11195
    20
    invent new nonces here, but he can also use NS1.  Common to
paulson@11195
    21
    all similar protocols.*)
paulson@11195
    22
  Fake :: "(state*state) set"
paulson@11195
    23
    "Fake == {(s,s').
paulson@11195
    24
	      EX B X. s' = Says Spy B X # s
paulson@11195
    25
		    & X: synth (analz (spies s))}"
paulson@11195
    26
  
paulson@11195
    27
  (*The numeric suffixes on A identify the rule*)
paulson@11195
    28
paulson@11195
    29
  (*Alice initiates a protocol run, sending a nonce to Bob*)
paulson@11195
    30
  NS1 :: "(state*state) set"
paulson@11195
    31
    "NS1 == {(s1,s').
paulson@11195
    32
	     EX A1 B NA.
paulson@11195
    33
	         s' = Says A1 B (Crypt (pubK B) {|Nonce NA, Agent A1|}) # s1
paulson@11195
    34
	       & Nonce NA ~: used s1}"
paulson@11195
    35
  
paulson@11195
    36
  (*Bob responds to Alice's message with a further nonce*)
paulson@11195
    37
  NS2 :: "(state*state) set"
paulson@11195
    38
    "NS2 == {(s2,s').
paulson@11195
    39
	     EX A' A2 B NA NB.
paulson@11195
    40
	         s' = Says B A2 (Crypt (pubK A2) {|Nonce NA, Nonce NB|}) # s2
paulson@11195
    41
               & Says A' B (Crypt (pubK B) {|Nonce NA, Agent A2|}) : set s2
paulson@11195
    42
	       & Nonce NB ~: used s2}"
paulson@11195
    43
 
paulson@11195
    44
  (*Alice proves her existence by sending NB back to Bob.*)
paulson@11195
    45
  NS3 :: "(state*state) set"
paulson@11195
    46
    "NS3 == {(s3,s').
paulson@11195
    47
	     EX A3 B' B NA NB.
paulson@11195
    48
	         s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3
paulson@11195
    49
               & Says A3  B (Crypt (pubK B) {|Nonce NA, Agent A3|}) : set s3
paulson@11195
    50
	       & Says B' A3 (Crypt (pubK A3) {|Nonce NA, Nonce NB|}) : set s3}"
paulson@11195
    51
paulson@11195
    52
paulson@11195
    53
paulson@11195
    54
constdefs
paulson@11195
    55
  Nprg :: state program
paulson@11195
    56
    (*Initial trace is empty*)
paulson@13812
    57
    "Nprg == mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
paulson@11195
    58
paulson@11195
    59
end