English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Many important cryptographic primitives offer probabilistic guarantees ofsecurity that can be specified as quantitative hyperproperties; these arespecifications that stipulate the existence of a certain number of traces inthe system satisfying certain constraints. Verification of such hyperpropertiesis extremely challenging because they involve simultaneous reasoning about anunbounded number of different traces. In this paper, we introduce a techniquefor verification of quantitative hyperproperties based on the notion of traceenumeration relations. These relations allow us to reduce the problem oftrace-counting into one of model-counting of formulas in first-order logic. Wealso introduce a set of inference rules for machine-checked reasoning about thenumber of satisfying solutions to first-order formulas (aka model counting).Putting these two components together enables semi-automated verification ofquantitative hyperproperties on infinite state systems. We use our methodologyto prove confidentiality of access patterns in Path ORAMs of unbounded size,soundness of a simple interactive zero-knowledge proof protocol as well asother applications of quantitative hyperproperties studied in past work.

Verification of Quantitative Hyperproperties Using Trace Enumeration Relations