Formal Verification for Cryptography Protocols

In this year's S&P conference, Microsoft and INRIA has proposed a paper "Implementing TLS with Verified Cryptographic Security." In this paper, an F# TLS library was implemented and serial of formal proof were  also given. To understand their survey, some background knowledge are necessary. After some search, the slide published in etaps12 is most easily document. So in this article, I will summary this slide.

Attack Model

The attack model is communication in an insecure network environment as following figure

• The attacker can intercept all messages sent on the network
• He can compute messages
• He can send messages on the network

The term cryptographic primitives means basic cryptographic function which later used to build security protocols.

Symbolic Model and Computational Model 

Model	Symbolic Model	Computational Model
Cryptographic Primitives	blackboxes	functions on bitstrings
Messages	terms on cryptographic primitives	bitstrings
Attack Capability	Compute with cryptographic primitives	Probabilistic polynomial-time Turing machine
Security Assumptions	Verify what attacker can do	Verify what attacker cannot do

Verifying Protocols in the Symbolic Model

The basic idea is to compute the knowledge of attacker. So we exhaust all combination of cryptographic primitives. Then check if any of them violate security policy. It is trivial that those combination can be infinite, thus this model can be undecidable. So some technique like approximation, proper subset or termination state are used.

For example, Horn Clauses can be use to verify symbolic model. With the notation attacker function
                                             attacker(M) means “the attacker may have M”

And there introduce two functions

       Construct f( m1 ,m2 ,m3 ,...,mn ) 

              attacker( m1 ) ^ attacker( m2 ) ^ ... ^ attacker( mn ) -> attacker( f(m1, m2,..., mn) )  

       Destruct g(m1,m2,...,mn) -> m

              attacker( m1 ) ^ attacker( m2 ) ^ ... ^ attacker( mn ) -> attacker( m )

       Example

              attacker(m) ∧ attacker(k) → attacker(sencrypt(m, k))

              attacker(sencrypt(m, k)) ∧ attacker(k) → attacker(m)

Verifying Protocols in the Computational Model

There are thee strategy to verify the computational model

1. Linking the symbolic and the computational models
   First, proof in symbolic model and verify computation soundness in symbolic model. Then we can prove the computatiobal model is secure. 
2. Adapting techniques from the symbolic models
   Some symbolic techniques can also be adapted to the computational model
3. Direct computational proofs
   Proofs in the computational model are typically proofs by sequences of games

Reference 

1. Bruno Blanchet's presentation slide(1)
   http://www.mpi-inf.mpg.de/vtsa11/slides/blanchet/VTSA11intro.pdf
2. Bruno Blanchet's presentation slide(2) 
   http://www.mpi-inf.mpg.de/vtsa11/slides/blanchet/VTSA11proverif.pdf
3. Bruno Blanchet's presentation slide(3)
   http://cs.ioc.ee/etaps12/invited/blanchet-slides.pdf