equal
deleted
inserted
replaced
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 = Public + NatPair: |
44 theory TLS imports Public NatPair begin |
45 |
45 |
46 constdefs |
46 constdefs |
47 certificate :: "[agent,key] => msg" |
47 certificate :: "[agent,key] => msg" |
48 "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}" |
48 "certificate A KA == Crypt (priSK Server) {|Agent A, Key KA|}" |
49 |
49 |