Advanced method for cryptographic protocol verification
Issue title: Selected papers from the International Conference on Computer Science, Software Engineering, Information Technology, e-Business, and Applications, 2004
Abstract: Based on a previous work using abstract interpretation for secret property verification, we propose a new method for protocol verification combining abstract interpretation for Input/Output set description and finite state machine for property propagation and verification. Generating Input/Output set for FSM is a bit difficult specially when one want to apply such technique on cryptographic protocol implementation. It is true that one can verify protocol specification, but in such case one cannot discover any significant logical follows introduced by implementation. To overcome this, we develop a particular semantic defined for cryptographic protocol verification, that facilitates verifying or detecting a large set of faults and attacks. Faults and attacks will be described as scenarios with a set of preconditions and post conditions. The FSM based method is used to discover a transition is possible from an initial set (inputs) to a final state describing a fault or a global attack state. This semantic along with the model and the verification tool SSPV allow the prove of more key security properties.
