Interrogator
Prolog program [MCF87, Mil95], state-transition model
Global state is composition of A-state, B-state, etc.
- Party state has component per variable: A, B, Ka, etc. plus the network buffer
- transition(state, msgIn, msgOut, nextState) defined by protocol
- Message is a Prolog list [A, B, enc(Ka, Na)]