Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Concept

Système de preuve interactive

Publications associées (17)

Orthologic with Axioms

Viktor Kuncak, Simon Guilloud

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Quantum Protocols for ML, Physics, and Finance

Grzegorz Adam Gluch

In this thesis, we give new protocols that offer a quantum advantage for problems in ML, Physics, and Finance. Quantum mechanics gives predictions that are inconsistent with local realism. The experiment proving this fact (Bell, 1964) gives a quantum proto ...

EPFL2024

Latency Interfaces for Systems Code

Rishabh Ramesh Iyer

This thesis demonstrates that it is feasible for systems code to expose a latency interface that describes its latency and related side effects for all inputs, just like the code's semantic interface describes its functionality and related side effects. S ...

EPFL2023

A Toolbox for Barriers on Interactive Oracle Proofs

Alessandro Chiesa

Interactive oracle proofs (IOPs) are a proof system model that combines features of interactive proofs (IPs) and probabilistically checkable proofs (PCPs). IOPs have prominent applications in complexity theory and cryptography, most notably to constructing ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

A PCP Theorem for Interactive Proofs and Applications

Alessandro Chiesa

The celebrated PCP Theorem states that any language in NP can be decided via a verifier that reads O(1) bits from a polynomially long proof. Interactive oracle proofs (IOP), a generalization of PCPs, allow the verifier to interact with the prover for multi ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Zero-Knowledge IOPs with Linear-Time Prover and Polylogarithmic-Time Verifier

Alessandro Chiesa

Interactive oracle proofs (IOPs) are a multi-round generalization of probabilistically checkable proofs that play a fundamental role in the construction of efficient cryptographic proofs. ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Spatial Isolation Implies Zero Knowledge Even in a Quantum World

Alessandro Chiesa

Zero knowledge plays a central role in cryptography and complexity. The seminal work of Ben-Or et al. (STOC 1988) shows that zero knowledge can be achieved unconditionally for any language in NEXP, as long as one is willing to make a suitable physical assu ...

ASSOC COMPUTING MACHINERY2022

On Succinct Non-interactive Arguments in Relativized Worlds

Alessandro Chiesa

Succinct non-interactive arguments of knowledge (SNARKs) are cryptographic proofs with strong efficiency properties. Applications of SNARKs often involve proving computations that include the SNARK verifier, a technique called recursive composition. Unfort ...

SPRINGER INTERNATIONAL PUBLISHING AG2022

Privacy-Preserving Federated Analytics using Multiparty Homomorphic Encryption

David Jules Froelicher

Analyzing and processing data that are siloed and dispersed among multiple distrustful stakeholders is difficult and can even become impossible when the data are sensitive or confidential. Current data-protection and privacy regulations highly restrict the ...

EPFL2021

Modeling Superlattices of Dipolar and Polarizable Semiconducting Nanoparticles

Federico Giberti

We present an analytical model to describe the stability of arbitrary semiconducting nanoparticle (NP) superlattices as a function of the dipole and polarizability of their constituents. We first validate our model by comparison with density functional the ...

AMER CHEMICAL SOC2019

Implications of Position in Cryptography

Handan Kilinç Alper

In our daily lives, people or devices frequently need to learn their location for many reasons as some services depend on the absolute location or the proximity. The outcomes of positioning systems can have critical effects e.g., on military, emergency. Th ...

EPFL2018

Artist-Oriented 3D Character Posing from 2D Strokes

Ronan Boulic, Benoît Le Callennec, Pawan Kumar Harish, Mentar Mahmudi

In this paper we present an intuitive tool suitable for 2D artists using touch-enabled pen tablets. An artist-oriented tool should be easy-to-use, real-time, versatile, and locally refinable. Our approach uses an interactive system for 3D character posing ...

Elsevier2016

Sound Proof of Proximity of Knowledge

Serge Vaudenay

Public-key distance bounding schemes are needed to defeat relay attacks in payment systems. So far, only five such schemes exist, but fail to fully protect against malicious provers. In this paper, we solve this problem. We provide a full formalism to defi ...

2015

On Modeling Terrorist Frauds

Serge Vaudenay

Quite recently, distance-bounding protocols received a lot of attention as they offer a good solution to thwart relay attacks. Their security models at still unstable, especially when considering terrorist fraud. This considers the case where a malicious p ...

Springer2013

Interactive multiview video system with low decoding complexity

Pascal Frossard, Thomas Maugey

Research in multimedia is always investigating new ways of improving the immersive experience of the users. One current solution consists in designing systems which offer a high level of interactivity, such as multiview content navigation where the point o ...

2011

Decision Procedures for Multisets with Cardinality Constraints

Viktor Kuncak, Ruzica Piskac

Applications in software verification and interactive theorem proving often involve reasoning about sets of objects. Cardinality constraints on such collections also arise in these scenarios. Multisets arise for analogous reasons as sets: abstracting the c ...

Springer2008

Linear Arithmetic with Stars

Viktor Kuncak, Ruzica Piskac

We consider an extension of integer linear arithmetic with a “star” operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and th ...

Springer2008

Publications associées (17)

SPRINGER INTERNATIONAL PUBLISHING AG2022