Subsequent Developments
Discussions and semantics, e.g., [Syv91]
More extensive logics, e.g., GNY (Gong-Needham-Yahalom) [GNY90] and SVO [SvO94]
GNY extensions:
- Unencrypted fields retained
- “P possesses X” construct and possession rules
- “not originated here” operator
- Rationality rule: if X |– Y then P bel X |– P bel Y
- “message extension” links fields to assertions
Mechanization of inference, e.g, [KW96, Bra96]
- User still does idealization
Protocol vs. idealization problem still unsolved