Towards verified quantum crypto

We are currently working towards the formal verification (using theorem provers) of the security of quantum cryptographic protocols. In this talk, I will describe the context of that research, our progress, and challenges faced. This will involve very little crypto, but a little bit of program logics.