equal
deleted
inserted
replaced
23 TTPAuth :: nat |
23 TTPAuth :: nat |
24 SAuth :: nat |
24 SAuth :: nat |
25 BothAuth :: nat |
25 BothAuth :: nat |
26 |
26 |
27 text{*We formalize a fixed way of computing responses. Could be better.*} |
27 text{*We formalize a fixed way of computing responses. Could be better.*} |
28 constdefs |
28 definition "response" :: "agent => agent => nat => msg" where |
29 "response" :: "agent => agent => nat => msg" |
|
30 "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" |
29 "response S R q == Hash {|Agent S, Key (shrK R), Nonce q|}" |
31 |
30 |
32 |
31 |
33 inductive_set certified_mail :: "event list set" |
32 inductive_set certified_mail :: "event list set" |
34 where |
33 where |