equal
deleted
inserted
replaced
6 header{*The Certified Electronic Mail Protocol by Abadi et al.*} |
6 header{*The Certified Electronic Mail Protocol by Abadi et al.*} |
7 |
7 |
8 theory CertifiedEmail imports Public begin |
8 theory CertifiedEmail imports Public begin |
9 |
9 |
10 abbreviation |
10 abbreviation |
11 TTP :: agent |
11 TTP :: agent where |
12 "TTP == Server" |
12 "TTP == Server" |
13 |
13 |
14 RPwd :: "agent => key" |
14 abbreviation |
|
15 RPwd :: "agent => key" where |
15 "RPwd == shrK" |
16 "RPwd == shrK" |
16 |
17 |
17 |
18 |
18 (*FIXME: the four options should be represented by pairs of 0 or 1. |
19 (*FIXME: the four options should be represented by pairs of 0 or 1. |
19 Right now only BothAuth is modelled.*) |
20 Right now only BothAuth is modelled.*) |