equal
deleted
inserted
replaced
70 (*sessionK is collision-free and makes symmetric keys. Also, no clientK |
70 (*sessionK is collision-free and makes symmetric keys. Also, no clientK |
71 clashes with any serverK.*) |
71 clashes with any serverK.*) |
72 inj_sessionK "inj sessionK" |
72 inj_sessionK "inj sessionK" |
73 |
73 |
74 isSym_sessionK "isSymKey (sessionK x)" |
74 isSym_sessionK "isSymKey (sessionK x)" |
75 |
|
76 (*serverK is similar*) |
|
77 inj_serverK "inj serverK" |
|
78 isSym_serverK "isSymKey (serverK x)" |
|
79 |
75 |
80 |
76 |
81 consts tls :: event list set |
77 consts tls :: event list set |
82 inductive tls |
78 inductive tls |
83 intrs |
79 intrs |