arXiv subjects

Dominique Unruh

Publications and source records attributed to Dominique Unruh.

12 recordsLinked to original sources

arXiv2026

Quantum Weakest Preconditions Revisited: Pre-expectations for Expected Runtime Analysis

Quantum weakest preconditions are a fundamental tool for program verification of quantum programs. Many variations have been reported in the literature. We revisit quantum weakest preconditions from the perspective of expected runtime analysis of quantum programs and introduce a novel pre-expectation framework that enables to reason about the preconditions of quantum programs without the need of an upper bound. This is particularly interesting for quantum programs involving reward statements. The overall goal is to analyze runtime behavior even in the case of programs with potentially infinite expected runtime. This paper presents several ways to do so, e.g., a program transformation such that the expected runtime of a quantum program can be expressed using the weakest pre-expectation calculus with rewards.

cs.LO↗

arXiv2025

Complex Bounded Operators in Isabelle/HOL

We present a formalization of bounded operators on complex vector spaces in Isabelle/HOL. Our formalization contains material on complex vector spaces (normed spaces, Banach spaces, Hilbert spaces) that complements and goes beyond the developments of real vectors spaces in the Isabelle/HOL standard library. We define the type of bounded operators between complex vector spaces (cblinfun) and develop the theory of unitaries, projectors, extension of bounded linear functions (BLT theorem), adjoints, Loewner order, closed subspaces and more. For the finite-dimensional case, we provide code generation support by identifying finite-dimensional operators with matrices as formalized in the Jordan_Normal_Form AFP entry.

cs.LO↗

arXiv2025

Bayesian Inference in Quantum Programs

Conditioning is a key feature in probabilistic programming to enable modeling the influence of data (also known as observations) to the probability distribution described by such programs. Determining the posterior distribution is also known as Bayesian inference. This paper equips a quantum while-language with conditioning, defines its denotational and operational semantics over infinite-dimensional Hilbert spaces, and shows their equivalence. We provide sufficient conditions for the existence of weakest (liberal) precondition-transformers and derive inductive characterizations of these transformers. It is shown how w(l)p-transformers can be used to assess the effect of Bayesian inference on (possibly diverging) quantum programs.

cs.LO↗

arXiv2024

Quantum references

We present a theory of "quantum references", similar to lenses in classical functional programming, that allow to point to a subsystem of a larger quantum system, and to mutate/measure that part. Mutable classical variables, quantum registers, and wires in quantum circuits are examples of this, but also references to parts of larger quantum datastructures. Quantum references in our setting can also refer to subparts of other references, or combinations of parts from different references, or quantum references seen in a different basis, etc. Our modeling is intended to be well suited for formalization in theorem provers and as a foundation for modeling variables in quantum programs. We study quantum references in greater detail and cover the infinite-dimensional case as well, but also provide a more general treatment not specific to the quantum case. We implemented a large part of our results (including a small quantum Hoare logic and an analysis of quantum teleportation) in the Isabelle/HOL theorem prover.

cs.LO↗

arXiv2021

Quantum Relational Hoare Logic with Expectations

We present a variant of the quantum relational Hoare logic from (Unruh, POPL 2019) that allows us to use "expectations" in pre- and postconditions. That is, when reasoning about pairs of programs, our logic allows us to quantitatively reason about how much certain pre-/postconditions are satisfied that refer to the relationship between the programs inputs/outputs.

cs.LO↗

arXiv2020

Local Variables and Quantum Relational Hoare Logic

We add local variables to quantum relational Hoare logic (Unruh, POPL 2019). We derive reasoning rules for supporting local variables (including an improved "adversary rule"). We extended the qrhl-tool for computer-aided verification of qRHL to support local variables and our new reasoning rules.

cs.LO↗

arXiv2019

Quantum Hoare Logic with Ghost Variables

Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces "ghost variables" to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.

quant-ph↗

arXiv2019

Quantum Relational Hoare Logic

We present a logic for reasoning about pairs of interactive quantum programs - quantum relational Hoare logic (qRHL). This logic follows the spirit of probabilistic relational Hoare logic (Barthe et al. 2009) and allows us to formulate how the outputs of two quantum programs relate given the relationship of their inputs. Probabilistic RHL was used extensively for computer-verified security proofs of classical cryptographic protocols. Since pRHL is not suitable for analyzing quantum cryptography, we present qRHL as a replacement, suitable for the security analysis of post-quantum cryptography and quantum protocols. The design of qRHL poses some challenges unique to the quantum setting, e.g., the definition of equality on quantum registers. Finally, we implemented a tool for verifying proofs in qRHL and developed several example security proofs in it.

quant-ph↗

arXiv2016

An adaptive attack on Wiesner's quantum money

Unlike classical money, which is hard to forge for practical reasons (e.g. producing paper with a certain property), quantum money is attractive because its security might be based on the no-cloning theorem. The first quantum money scheme was introduced by Wiesner circa 1970. Although more sophisticated quantum money schemes were proposed, Wiesner's scheme remained appealing because it is both conceptually clean and relatively easy to implement. We show efficient adaptive attacks on Wiesner's quantum money scheme [Wie83] (and its variant by Bennett et al. [BBBW83]), when valid money is accepted and passed on, while invalid money is destroyed. We propose two attacks, the first is inspired by the Elitzur-Vaidman bomb testing problem [EV93, KWH+95], while the second is based on the idea of protective measurements [AAV93]. It allows us to break Wiesner's scheme with 4 possible states per qubit, and generalizations which use more than 4 states per qubit.

quant-ph↗

arXiv2014

Quantum Attacks on Classical Proof Systems - The Hardness of Quantum Rewinding

Quantum zero-knowledge proofs and quantum proofs of knowledge are inherently difficult to analyze because their security analysis uses rewinding. Certain cases of quantum rewinding are handled by the results by Watrous (SIAM J Comput, 2009) and Unruh (Eurocrypt 2012), yet in general the problem remains elusive. We show that this is not only due to a lack of proof techniques: relative to an oracle, we show that classically secure proofs and proofs of knowledge are insecure in the quantum setting. More specifically, sigma-protocols, the Fiat-Shamir construction, and Fischlin's proof system are quantum insecure under assumptions that are sufficient for classical security. Additionally, we show that for similar reasons, computationally binding commitments provide almost no security guarantees in a quantum setting. To show these results, we develop the "pick-one trick", a general technique that allows an adversary to find one value satisfying a given predicate, but not two.

quant-ph↗

arXiv2009

Universally Composable Quantum Multi-Party Computation

The Universal Composability model (UC) by Canetti (FOCS 2001) allows for secure composition of arbitrary protocols. We present a quantum version of the UC model which enjoys the same compositionality guarantees. We prove that in this model statistically secure oblivious transfer protocols can be constructed from commitments. Furthermore, we show that every statistically classically UC secure protocol is also statistically quantum UC secure. Such implications are not known for other quantum security definitions. As a corollary, we get that quantum UC secure protocols for general multi-party computation can be constructed from commitments.

quant-ph↗

arXiv2004

Simulatable security for quantum protocols

The notion of simulatable security (reactive simulatability, universal composability) is a powerful tool for allowing the modular design of cryptographic protocols (composition of protocols) and showing the security of a given protocol embedded in a larger one. Recently, these methods have received much attention in the quantum cryptographic community. We give a short introduction to simulatable security in general and proceed by sketching the many different definitional choices together with their advantages and disadvantages. Based on the reactive simulatability modelling of Backes, Pfitzmann and Waidner we then develop a quantum security model. By following the BPW modelling as closely as possible, we show that composable quantum security definitions for quantum protocols can strongly profit from their classical counterparts, since most of the definitional choices in the modelling are independent of the underlying machine model. In particular, we give a proof for the simple composition theorem in our framework.

quant-ph↗