What exactly is Symbolic Model Checking?

I know that Symbolic Model Checking is state space traversal based on representations of states sets and transition relations as formulas like in CTL using models like Kripke Model. I know the theory. But I'm finding it hard to understand the actual application. Where exactly is it used? What exactly does it do and how does it work?

Can someone explain with a real example and relate theory to practice?

Symbolic model checking can be very useful for verifying the correctness of communications and security protocols. For example:

• A symbolic model of an OAUTH2 implementation could help check for unintended consequences where an adversary obtains secret authentication tokens or related circumstantial data that could help them contravene the process.

• A symbolic model of a cryptographic protocol, such as a TLS handshake, could help verify that the cryptographic design doesn't have any unintended consequences.

This works by writing a symbolic description of all the primitive functions and protocol algorithms, and then having a symbolic model checker, such as ProVerif, traverse the state space and attempt to detect state combinations that produce unfavorable results. In the case of ProVerif, symbolic models are described using the applied Pi calculus as the modeling language. This allows the description of protocols in a functional, ML-like syntax.

StackExchange Computer Science Q#40636, answer score: 6