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