Modelling and Analysis of Quantum Cryptographic Protocols

Speaker: Simon Gay

29th November 2005 , 4pm , Devonshire G21/G22 Conference Room

Abstract

Most current cryptographic techniques rely on unproven assumptions about the computational intractability of tasks such as prime factorisation. These assumptions are directly threatened by theoretical developments in quantum computing, which could become practical in the medium term. Quantum cryptography is therefore of great interest as it is provably secure even in the presence of quantum computers. After introducing the basic concepts of quantum computing and quantum cryptography, I will argue that there is a need for formal modelling and analysis of quantum cryptographic protocols (as distinct from primitives) if we are to be confident of the security of real implemented systems. I will present recent work in this direction, including the design of a process calculus for modelling quantum systems, and preliminary results on model-checking quantum systems.