Symbolic Analysis of Cryptographic Protocols:Models, Methods, and Soundness
Morten Dahl · 2013
We present our work on using abstract models for formally analysing cryptographic protocols: First, we present an ecient method for verifying trace-based authenticity properties of protocols using nonces, symmetric encryption, and asymmetric encryption. The method is based on a type system of Gordon et al., which we modify to support fully-automated type inference. Tests conducted via an implementation of our algorithm found it to be very ecient. Second, we show how privacy may be captured in a symbolic model using an equivalencebased property and give a formal denition. We formalise a concrete protocol by Blumberg et al. using one-way functions and commitments for providing various location based vehicle services, and report on our ndings and experience of carrying out its analysis using the ProVerif tool. Third, we make an abstract model of the powerful simulation-based Universally Compos- able framework by Canetti for specifying and analysing protocols, and show that our model is sound with respect to its standard computational interpretation. Our model supports powerful primitives such as homomorphic encryption and non-interactive zero-knowledge proofs, which we show may be used to implement several interesting two-party functionalities. As a case study we use the ProVerif tool to analyse an oblivious transfer protocol by Damgard et al. under static corruption