1.1 --- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -16,40 +16,48 @@
     1.4  subsection{*messages used in the protocol*}
     1.5  
     1.6  abbreviation
     1.7 -  nil :: "msg"
     1.8 +  nil :: "msg" where
     1.9    "nil == Number 0"
    1.10  
    1.11 -  or1 :: "agent => agent => nat => event"
    1.12 +abbreviation
    1.13 +  or1 :: "agent => agent => nat => event" where
    1.14    "or1 A B NA ==
    1.15      Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}"
    1.16  
    1.17 -  or1' :: "agent => agent => agent => nat => msg => event"
    1.18 +abbreviation
    1.19 +  or1' :: "agent => agent => agent => nat => msg => event" where
    1.20    "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}"
    1.21  
    1.22 -  or2 :: "agent => agent => nat => nat => msg => event"
    1.23 +abbreviation
    1.24 +  or2 :: "agent => agent => nat => nat => msg => event" where
    1.25    "or2 A B NA NB X ==
    1.26      Says B Server {|Nonce NA, Agent A, Agent B, X,
    1.27                      Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    1.28  
    1.29 -  or2' :: "agent => agent => agent => nat => nat => event"
    1.30 +abbreviation
    1.31 +  or2' :: "agent => agent => agent => nat => nat => event" where
    1.32    "or2' B' A B NA NB ==
    1.33      Says B' Server {|Nonce NA, Agent A, Agent B,
    1.34                       Ciph A {|Nonce NA, Agent A, Agent B|},
    1.35                       Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}"
    1.36  
    1.37 -  or3 :: "agent => agent => nat => nat => key => event"
    1.38 +abbreviation
    1.39 +  or3 :: "agent => agent => nat => nat => key => event" where
    1.40    "or3 A B NA NB K ==
    1.41      Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|},
    1.42                      Ciph B {|Nonce NB, Key K|}|}"
    1.43  
    1.44 -  or3':: "agent => msg => agent => agent => nat => nat => key => event"
    1.45 +abbreviation
    1.46 +  or3':: "agent => msg => agent => agent => nat => nat => key => event" where
    1.47    "or3' S Y A B NA NB K ==
    1.48      Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}"
    1.49  
    1.50 -  or4 :: "agent => agent => nat => msg => event"
    1.51 +abbreviation
    1.52 +  or4 :: "agent => agent => nat => msg => event" where
    1.53    "or4 A B NA X == Says B A {|Nonce NA, X, nil|}"
    1.54  
    1.55 -  or4' :: "agent => agent => nat => key => event"
    1.56 +abbreviation
    1.57 +  or4' :: "agent => agent => nat => key => event" where
    1.58    "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}"
    1.59  
    1.60  subsection{*definition of the protocol*}