1

An interactive prover for protocol verification in the computational model (To appear)

Oracle simulation: a technique for protocol composition with long term shared secrets

Universal equivalence and majority on probabilistic programs over finite fields

We study equivalence checking of probabilistic programs, a fundamental problem which arises in many application areas including cryptography, privacy, algorithmic fairness and machine learning. The programming language we consider manipulates …

Symbolic methods in computational cryptography proofs

Code-based game-playing is a popular methodology for proving security of cryptographic constructions and side-channel countermeasures. This methodology relies on treating cryptographic proofs as an instance of relational program verification (between …

Symbolic Proofs for Lattice-Based Cryptography

An extensive formal analysis of multi-factor authentication protocols

Passwords are still the most widespread means for authenticating users, even though they have been shown to create huge security problems. This motivated the use of additional authentication mechanisms used in so-called multi-factor authentication …

Symbolic Models for Isolated Execution Environments

Isolated Execution Environments (IEEs), such as ARM TrustZone and Intel SGX, offer the possibility to execute sensitive code in isolation from other malicious programs, running on the same machine, or a potentially corrupted OS. A key feature of IEEs …