A Logic of Interactive Proofs

Abstract

The introduction of interactive proofs by Goldwasser et al. ([1]) poses an inter- esting question to the already vividly researched area of uncertain reasoning and justification logic - How can we quantitatively describe an evidence transforma- tion that gets progressively more meaningful and how can we model agents that reason based on such transformed evidence? In this work, we introduce the probabilistic two-agent justification logic IPJ, a logic in which we can reason about agents that perform interactive proofs. We present its syntax and semantics and provide a soundness proof. Moreover, we investigate how our axiomatisation can be extended in order to capture a weaker notion of the zero-knowledge property of interactive proofs. The foun- dation of our logic is built on the works of Kokkinis et al. ([2]) and Ognjanovi ́c et al. ([3]) who developed a probabilistic justification logic PJ and its extension CPJL which allows for conditional and non-standard probabilities. We answer the question above by parametrizing our logic over the set of negligi- ble functions f (n) = n−kfor all k ∈N. This approach enables us to canonically construct the set of formulas that are known by the agents to be interactively provable. By doing so, we closely model the soundness and completeness proper- ties of interactive proofs which are usually stated by using first-order quantifiers. Furthermore, we use non-standard probabilities in order to model the limit cases of the aforementioned properties.