13 |
13 |
14 theory Guard_OtwayRees imports Guard_Shared begin |
14 theory Guard_OtwayRees imports Guard_Shared begin |
15 |
15 |
16 subsection{*messages used in the protocol*} |
16 subsection{*messages used in the protocol*} |
17 |
17 |
18 syntax nil :: "msg" |
18 abbreviation |
|
19 nil :: "msg" |
|
20 "nil == Number 0" |
19 |
21 |
20 translations "nil" == "Number 0" |
22 or1 :: "agent => agent => nat => event" |
|
23 "or1 A B NA == |
|
24 Says A B {|Nonce NA, Agent A, Agent B, Ciph A {|Nonce NA, Agent A, Agent B|}|}" |
21 |
25 |
22 syntax or1 :: "agent => agent => nat => event" |
26 or1' :: "agent => agent => agent => nat => msg => event" |
|
27 "or1' A' A B NA X == Says A' B {|Nonce NA, Agent A, Agent B, X|}" |
23 |
28 |
24 translations "or1 A B NA" |
29 or2 :: "agent => agent => nat => nat => msg => event" |
25 => "Says A B {|Nonce NA, Agent A, Agent B, |
30 "or2 A B NA NB X == |
26 Ciph A {|Nonce NA, Agent A, Agent B|}|}" |
31 Says B Server {|Nonce NA, Agent A, Agent B, X, |
27 |
|
28 syntax or1' :: "agent => agent => agent => nat => msg => event" |
|
29 |
|
30 translations "or1' A' A B NA X" |
|
31 => "Says A' B {|Nonce NA, Agent A, Agent B, X|}" |
|
32 |
|
33 syntax or2 :: "agent => agent => nat => nat => msg => event" |
|
34 |
|
35 translations "or2 A B NA NB X" |
|
36 => "Says B Server {|Nonce NA, Agent A, Agent B, X, |
|
37 Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" |
32 Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" |
38 |
33 |
39 syntax or2' :: "agent => agent => agent => nat => nat => event" |
34 or2' :: "agent => agent => agent => nat => nat => event" |
40 |
35 "or2' B' A B NA NB == |
41 translations "or2' B' A B NA NB" |
36 Says B' Server {|Nonce NA, Agent A, Agent B, |
42 => "Says B' Server {|Nonce NA, Agent A, Agent B, |
|
43 Ciph A {|Nonce NA, Agent A, Agent B|}, |
37 Ciph A {|Nonce NA, Agent A, Agent B|}, |
44 Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" |
38 Ciph B {|Nonce NA, Nonce NB, Agent A, Agent B|}|}" |
45 |
39 |
46 syntax or3 :: "agent => agent => nat => nat => key => event" |
40 or3 :: "agent => agent => nat => nat => key => event" |
47 |
41 "or3 A B NA NB K == |
48 translations "or3 A B NA NB K" |
42 Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|}, |
49 => "Says Server B {|Nonce NA, Ciph A {|Nonce NA, Key K|}, |
|
50 Ciph B {|Nonce NB, Key K|}|}" |
43 Ciph B {|Nonce NB, Key K|}|}" |
51 |
44 |
52 syntax or3':: "agent => msg => agent => agent => nat => nat => key => event" |
45 or3':: "agent => msg => agent => agent => nat => nat => key => event" |
|
46 "or3' S Y A B NA NB K == |
|
47 Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}" |
53 |
48 |
54 translations "or3' S Y A B NA NB K" |
49 or4 :: "agent => agent => nat => msg => event" |
55 => "Says S B {|Nonce NA, Y, Ciph B {|Nonce NB, Key K|}|}" |
50 "or4 A B NA X == Says B A {|Nonce NA, X, nil|}" |
56 |
51 |
57 syntax or4 :: "agent => agent => nat => msg => event" |
52 or4' :: "agent => agent => nat => key => event" |
58 |
53 "or4' B' A NA K == Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}" |
59 translations "or4 A B NA X" => "Says B A {|Nonce NA, X, nil|}" |
|
60 |
|
61 syntax or4' :: "agent => agent => nat => msg => event" |
|
62 |
|
63 translations "or4' B' A NA K" => |
|
64 "Says B' A {|Nonce NA, Ciph A {|Nonce NA, Key K|}, nil|}" |
|
65 |
54 |
66 subsection{*definition of the protocol*} |
55 subsection{*definition of the protocol*} |
67 |
56 |
68 consts or :: "event list set" |
57 consts or :: "event list set" |
69 |
58 |