39 Notes A {|Agent B, Nonce PMS|}. |
39 Notes A {|Agent B, Nonce PMS|}. |
40 *) |
40 *) |
41 |
41 |
42 header{*The TLS Protocol: Transport Layer Security*} |
42 header{*The TLS Protocol: Transport Layer Security*} |
43 |
43 |
44 theory TLS imports Public Nat_Int_Bij begin |
44 theory TLS imports Public Nat_Bijection begin |
45 |
45 |
46 definition certificate :: "[agent,key] => msg" where |
46 definition certificate :: "[agent,key] => msg" where |
47 "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}" |
47 "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}" |
48 |
48 |
49 text{*TLS apparently does not require separate keypairs for encryption and |
49 text{*TLS apparently does not require separate keypairs for encryption and |
72 |
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). prod_encode(x, prod_encode(y,z))"]) |
78 apply (simp add: inj_on_def) |
78 apply (simp add: inj_on_def prod_encode_eq) |
79 apply (blast dest!: nat2_to_nat_inj [THEN injD]) |
|
80 done |
79 done |
81 |
80 |
82 specification (sessionK) |
81 specification (sessionK) |
83 inj_sessionK: "inj sessionK" |
82 inj_sessionK: "inj sessionK" |
84 --{*sessionK is collision-free; also, no clientK clashes with any serverK.*} |
83 --{*sessionK is collision-free; also, no clientK clashes with any serverK.*} |
85 apply (rule exI [of _ |
84 apply (rule exI [of _ |
86 "%((x,y,z), r). nat2_to_nat(role_case 0 1 r, |
85 "%((x,y,z), r). prod_encode(role_case 0 1 r, |
87 nat2_to_nat(x, nat2_to_nat(y,z)))"]) |
86 prod_encode(x, prod_encode(y,z)))"]) |
88 apply (simp add: inj_on_def split: role.split) |
87 apply (simp add: inj_on_def prod_encode_eq split: role.split) |
89 apply (blast dest!: nat2_to_nat_inj [THEN injD]) |
|
90 done |
88 done |
91 |
89 |
92 axioms |
90 axioms |
93 --{*sessionK makes symmetric keys*} |
91 --{*sessionK makes symmetric keys*} |
94 isSym_sessionK: "sessionK nonces \<in> symKeys" |
92 isSym_sessionK: "sessionK nonces \<in> symKeys" |