Observations
According to “Rejoinder” [BAN90b], “There is no attempt to deal with … unauthorized release of secrets”
The logic is monotonic: if a key is believed to be good, the belief cannot be retracted
The protocol may be inconsistent with beliefs about confidentiality of keys and other secrets
More generally - one should analyze the protocol for consistency with its idealization
Alternatively - devise restrictions on protocols and idealization rules that guarantee consistency