src/HOL/Auth/Guard/Guard_NS_Public.thy
changeset 21404 eb85850d3eb7
parent 20768 1d478c2d621f
child 23746 a455e69c31cc
     1.1 --- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -18,19 +18,23 @@
     1.4  subsection{*messages used in the protocol*}
     1.5  
     1.6  abbreviation (input)
     1.7 -  ns1 :: "agent => agent => nat => event"
     1.8 +  ns1 :: "agent => agent => nat => event" where
     1.9    "ns1 A B NA == Says A B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    1.10  
    1.11 -  ns1' :: "agent => agent => agent => nat => event"
    1.12 +abbreviation (input)
    1.13 +  ns1' :: "agent => agent => agent => nat => event" where
    1.14    "ns1' A' A B NA == Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|})"
    1.15  
    1.16 -  ns2 :: "agent => agent => nat => nat => event"
    1.17 +abbreviation (input)
    1.18 +  ns2 :: "agent => agent => nat => nat => event" where
    1.19    "ns2 B A NA NB == Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    1.20  
    1.21 -  ns2' :: "agent => agent => agent => nat => nat => event"
    1.22 +abbreviation (input)
    1.23 +  ns2' :: "agent => agent => agent => nat => nat => event" where
    1.24    "ns2' B' B A NA NB == Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|})"
    1.25  
    1.26 -  ns3 :: "agent => agent => nat => event"
    1.27 +abbreviation (input)
    1.28 +  ns3 :: "agent => agent => nat => event" where
    1.29    "ns3 A B NB == Says A B (Crypt (pubK B) (Nonce NB))"
    1.30  
    1.31