equal
deleted
inserted
replaced
61 to avoid duplicating their properties. They are distinguished by a |
61 to avoid duplicating their properties. They are distinguished by a |
62 tag (not a bool, to avoid the peculiarities of if-and-only-if). |
62 tag (not a bool, to avoid the peculiarities of if-and-only-if). |
63 Session keys implicitly include MAC secrets.*) |
63 Session keys implicitly include MAC secrets.*) |
64 sessionK :: "(nat*nat*nat) * role => key" |
64 sessionK :: "(nat*nat*nat) * role => key" |
65 |
65 |
66 syntax |
66 abbreviation |
67 clientK :: "nat*nat*nat => key" |
67 clientK :: "nat*nat*nat => key" |
68 serverK :: "nat*nat*nat => key" |
68 "clientK X == sessionK(X, ClientRole)" |
69 |
69 |
70 translations |
70 serverK :: "nat*nat*nat => key" |
71 "clientK X" == "sessionK(X, ClientRole)" |
71 "serverK X == sessionK(X, ServerRole)" |
72 "serverK X" == "sessionK(X, ServerRole)" |
72 |
73 |
73 |
74 specification (PRF) |
74 specification (PRF) |
75 inj_PRF: "inj PRF" |
75 inj_PRF: "inj PRF" |
76 --{*the pseudo-random function is collision-free*} |
76 --{*the pseudo-random function is collision-free*} |
77 apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"]) |
77 apply (rule exI [of _ "%(x,y,z). nat2_to_nat(x, nat2_to_nat(y,z))"]) |