Interrogator, cont’d
Analysis technique
- Indicate what data item X is to be kept secret
- Define a pattern term for an INSECURE state: BadState
- Prolog query: pKnows(X, BadState, MsgHistory)
- Prolog will search for MsgHistory with an attack
Features:
- Interactive control of search
- Output protocol diagrams
Limitations
- Need specific goal state to reduce search time
- Risk of nontermination, due partly to Prolog depth-first search
- Handles only one session per party without special encoding