Interactive Theorem Proving for Quantum Cryptography, Security, and Active Objects.
by Florian Kammüller, Middlesex University London and TU Berlin
Inria Sophia Antipolis, 24.4.2015
In this presentation, I give an overview of interactive theorem proving and
its application in Software and Security Engineering. I first introduce
Higher Order Logic theorem provers, in particular Isabelle and Coq and the principles
underlying their application to object logics.
As a first case study, I present our current efforts on formalizing Quantum Protocols
with Coq and Isabelle. I give a brief overview of the background of this application,
the main ideas of the mathematical model and how it is formalized, showing first
results, e.g. quantum teleportation, but also shortcomings, and future plans.
In the second part, I give an overview of our other projects on security
protocol verification and formal analysis of insider threats. I finally show
how we use Isabelle/HOL to analyse programming languages, in particular active
object languages like ASPfun and MultiASP: defining syntax, semantics and type
systems in the interactive theorem prover, we mechanically prove properties of
well-formedness, type safety, and security.