4HTML>
Summary
Summary
Cryptographic protocol verification is based on models where
- Encryption is perfect (strong encryption)
- The attacker intercepts all messages (strong attacker)
- Security is undecidable in general, primarily because the number of sessions is unbounded.
Belief logic analysis:
- Requires “idealization” of the protocol
- Does not address confidentiality
- Can be peformed easily, manually or with automated support
State-exploration approaches
- Use model-checking tools
- Are effective for finding flaws automatically
- Are limited by finiteness