Model Checking for Cyber Security

1. Why Model Checking?
 - to ensure a software is secure
  => think hard about possible attack scenarios
  => what if you missed a possible attack?
  => Did you implement the attacks correctly?
 - The general correctness problem: Does the system meet the specification?

2. Formal methods
 - A different approach to correctness
  => Correctness problem is same
  => determine whether system meets the specification
  => However, system, specification must be mathematically precise
     Establishing correctness = proof
                                "Mathematically complete argument that system meets specification"
  => Proofs are hard! They require deep expertise
     ...Maybe they can be automated? but, it is impossible to prove everything automatically
  => but maybe some can?

http://ecomputernotes.com/software-engineering/formal-methods-model

3. Model Checking
 : Automated proofs of correctness
 : An automatic verification technique for finite state concurrent systems
 - Systems: Finite-state Kripke structures
  e.g. Dining Philosophers
 - Specifications: Temporal logic
 * LTL: Linear Time Logic 

4.Model Checking and Security
 : Model checking detects (automatically) if given finite-state system satisfies TL formulas
 - How can this be used to check system security?
  1) Formulate desired security properties in TL
  2) Model system and possible intruders
  3) Check if system satisfies formulas

http://seclab.stanford.edu/pcl/mc/mc.html

5. Needham-Schroeder Protocol / Needham-Schroeder Protocol with Lowe's fix
 : establish authenticated connection between A (initiator) and B (responder)

http://www.slashroot.in/needham-schroeder-protocol-explained

http://proverif.rocq.inria.fr/index.php