Michael Backes
Prof. Dr. | Faculty

  • Information Security and Cryptography
  • Building E9 1, Room 3.01
  • +49 681 302 3249
  • +49 681 302 57365
  • backes(aeht)mpi-sws.org
  • Personal Webpage

Curriculum Vitae

Michael Backes is the director of the Center for IT-Security, Privacy, and Accountability (CISPA) and a full professor at the Computer Science Department of Saarland University where he holds the chair for Information Security and Cryptography. He is moreover a Max Planck Fellow of the Max Planck Institute for Software Systems, the speaker of the SFB on Methods and Tools for Understanding and Controlling Privacy, and a Principal Investigator and Vice-coordinator of the Cluster of Excellence on Multimodal Computing and Interaction (MMCI).


  • 2004 – IBM Outstanding Achievement Award for contributions to Enterprise Privacy Architectures;
  • 2004 – Microsoft Award for outstanding research in privacy enhancing technologies;
  • 2005 – IBM Research Division Award for contributions to Web Services Security;
  • 2007 – Fellow of the Max Planck Society;
  • 2007 – CS Teaching Award of Saarland University;
  • 2008 – IBM Faculty Award;
  • 2009 – ERC Starting Grant;
    END2END Security
  • 2009 – MIT TR35;
  • 2009 – CS Teaching Award of Saarland University;
  • 2011 – IEEE Outstanding Community Award;
  • 2013 – ERC Synergy Grant;
    imPACT: Privacy, Accountability, Compliance, and Trust in Tomorrow's Internet
  • 2014 – IEEE Outstanding Community Award;
  • 2014 – CS Teaching Award of Saarland University;
  • 2014 – acatech Academy Membership;
  • 2017 – CNIL-Inria Award for Privacy Protection 2016;
    CNIL-Inria Award for Privacy Protection for his paper \"ADSNARK: nearly practical and privacy-preserving proofs on authenticated data\" (Co-authors: Manuel Barbosa, Dario Fiore, and Raphael M. Reischuk).



Reconciling Privacy and Utility in Continuous-Time Diffusion Networks

Lessons Learned from Using an Online Platform to Conduct Large-Scale, Online Controlled Security Experiments with Software Developers

Identifying Personal DNA Methylation Profiles by Genotype Inference

Comparing the Usability of Cryptographic APIs

Stack Overflow Considered Harmful? The Impact of Copy&Paste on Android Application Security

LUNA: Quantifying and Leveraging Uncertainty in Android Malware Analysis through Bayesian Machine Learning

ARTist: The Android Runtime Instrumentation and Security Toolkit

Efficient and Flexible Discovery of PHP Application Vulnerabilities

A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange

How Internet Resources Might Be Helping You Develop Faster but Less Securely

Who Controls the Internet? Analyzing Global Threats using Property Graph Traversals

Dachshund: Digging for and Securing (Non-)Blinded Constants in JIT Code

Unleashing Use-Before-Initialization Vulnerabilities in the Linux Kernel Using Targeted Stack Spraying

How the Web Tangled Itself: Uncovering the History of Client-Side Web (In)Security

Adversarial Examples for Malware Detection

On the (Statistical) Detection of Adversarial Examples

A Stitch in Time: Supporting Android Developers in Writing Secure Code

Keep me Updated: An Empirical Study of Third-Party Library Updatability on Android

textscDeemon: Detecting CSRF with Dynamic Analysis and Property Graphs

The ART of App Compartmentalization: Compiler-based Library Privilege Separation on Stock Android

walk2friends: Inferring Social Links from Mobility Profiles.

Verifying Security Policies in Multi-agent Workflows with Loops


Adversarial Perturbations Against Deep Neural Networks for Malware Classification

Simulating the Large-Scale Erosion of Genomic Privacy Over Time

Efficient Cryptographic Password Hardening Services From Partially Oblivious Commitments

Identifying the Scan and Attack Infrastructures behind Amplification DDoS attacks

Membership Privacy in MicroRNA-based Studies

Computational Soundness of Dalvik Bytecode

Reliable Third-Party Library Detection in Android and its Security Applications

Profile Linkability despite Anonymity in Social Media Systems

On the Feasibility of TTL-based Filtering for DRDoS Mitigation

A Survey on Routing in Anonymous Communication Protocols

Hey, You Have a Problem: On the Feasibility of Large-Scale Web Vulnerability Notification

On Demystifying the Android Application Framework: Re-Visiting Android Permission Specification Analysis

Privacy in Epigenetics: Temporal Linkability of MicroRNA Expression Profiles

What Cannot be Read, Cannot be Leveraged? Revisiting Assumptions of JIT-ROP Defenses

Detecting Hardware-Assisted Virtualization

Boxify: Bringing Full-Fledged App Sandboxing to Stock Android

R-Droid: Leveraging Android App Analysis with Static Slice Optimization

RamCrypt: Kernel-based Address Space Encryption for User-mode Processes

SoK: Lessons Learned From Android Security Research For Appified Software Platforms

You Get Where You're Looking For: The Impact Of Information Sources On Code Security

Implementation-level Analysis of the JavaScript Helios Voting Client

How to Make ASLR Win the Clone Wars: Runtime Re-Randomization

Anonymous RAM

From Zoos to Safaris - From Closed-World Enforcement to Open-World Assessment of Privacy

Delegatable Functional Signatures


Your Choice MATor(s): Large-scale Quantitative Anonymity Assessment of Tor Path Selection Algorithms Against Structural Attacks

Boxify: Full-fledged App Sandboxing for Stock Android

Symbolic Malleable Zero-knowledge Proofs

Oblivion: Mitigating Privacy Leaks by Controlling the Discoverability of Online Information

ADSNARK: Nearly-Practical Privacy-Preserving Proofs on Authenticated Data

PriCL: Creating a Precedent. A Framework for Reasoning about Privacy Case Law

How well do you blend into the crowd? - d-convergence: A novel paradigm for quantifying privacy in the age of Big-Data

Fully Secure Inner-Product Proxy Re-Encryption with constant size Ciphertext

Data Lineage in Malicious Environments

Quantifying Information Flow in Cryptographic Systems

Computational Soundness for Interactive Primitves

Secrecy without Perfect Randomness: Cryptography with (Bounded) Weak Sources

Oblivion: Mitigating Privacy Leaks by Controlling the Discoverability of Online Information


Android Security Framework: Extensible Multi-Layered Access Control on Android

Scippa: System-Centric IPC Provenance on Android

(Nothing else) MATor(s): Monitoring the Anonymity of Tor's Path Selection

You Can Run but You Can't Read: Preventing Disclosure Exploits in Executable Code

Lime: Data Lineage in the Malicious Environment

Oxymoron: Making Fine-Grained Memory Randomization Practical by Allowing Code Sharing

TUC: Time-sensitive and Modular Analysis of Anonymous Communication

Asynchronous MPC with a Strict Honest Majority Using Non-equivocation

WebTrust - A Comprehensive Authenticity and Integrity Framework for HTTP

BackRef: Accountability in Anonymous Communication Networks

X-pire 2.0 - A User-Controlled Expiration Date and Copy Protection Mechanism.

Computational Soundness Results for ProVerif - Bridging the Gap from Trace Properties to Uniformity

A Case Study of Research through the App Store: Leveraging the System UI as a Playing Field for Improving the Design of Smartphone Launchers


Using Mobile Device Communication to Strengthen e-Voting Protocols

Verifiable Delegation of Computation on Outsourced Data

AppGuard – Fine-grained Policy Enforcement for Untrusted Android Applications

Differentially Private Smart Metering with Battery Recharging

AnoA: A Framework For Analyzing Anonymous Communication Protocols

Computational Soundness of Symbolic Zero-Knowledge Proofs: Weaker Assumptions and Mechanized Verification

Preventing Side-Channel Leaks in Web Traffic: A Formal Approach

AppGuard - Enforcing User Requirements on Android Apps

Callee-site Rewriting of Sealed System Libraries

Privacy-Preserving Accountable Computation

Asynchronous Computational VSS with Reduced Communication Complexity

Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Secure Protocol Implementations

Idea: Callee-Site Rewriting of Sealed System Libraries


Computational Soundness without Protocol Restrictions

Ace: An Efficient Key-Exchange Protocol for Onion Routing

Brief announcement: distributed cryptography using trinc

Verified Security of Merkle-Damgård

ObliviAd: Provably Secure and Practical Online Behavioral Advertising

Automated Synthesis of Secure Distributed Applications

Provably Secure and Practical Onion Routing

Adding query privacy to robust DHTs

SAFE Extensibility of Data-Driven Web Applications

On the Development and Formalization of an Extensible Code Generator for Real Life Security Protocols

Diffusion-Based Image Compression in Steganography


A Security API for Distributed Social Networks

Non-Uniform Distributions in Quantitative Information-Flow

A Local Cross-Site Scripting Attack against Android Phones

Automatically Verifying Typing Constraints for a Data Processing Language

Cryptographically sound security proofs for basic and public-key Kerberos

Computational Verifiable Secret Sharing Revisited

CAMA: A Predictable Cache-Aware Memory Allocator

Securing social networks

G2C: Cryptographic Protocols from Goal-Driven Specifications

X-pire! - A digital expiration date for images in social networks

Union and Intersection Types for Secure Protocol Implementations


Computational Soundness of Symbolic Zero-Knowledge Proofs

Computationally Sound Abstraction and Verification of Secure Multi-Party Computations

Computationally Sound Verification of Source Code

Speaker Recognition in Encrypted Voice-over-IP Traffic

RatFish: A File Sharing Protocol Provably Secure Against Rational Users

Anonymity and Trust in Distributed Systems

Acoustic Side-Channel Attacks of Printers

Anonymous Webs of Trust


CoSP: a general framework for computational soundness proofs

CSAR: A practical and provable technique to make randomized systems accountable

Anonymous and Censorship-resistant Content-sharing in Unstructured Overlays

Achieving Security Despite Compromise Using Zero-knowledge

Automatic Discovery and Quantification of Information Leaks

Tempest in a Teapot: Compromising Reflections Revisited

Design and Verification of Anonymous Trust Protocols

Anonymity and Censorship Resistance in Unstructured Overlay Networks


Gespiegelt / Verräterische Reflexionen: Wie Brillengläser Geheimnisse verraten

A Formal Language for Cryptographic Pseudocode

Compromising Reflections or How to Read LCD Monitors Around the Corner

Computational Soundness of Symbolic Zero-Knowledge Proofs Against Active Attackers

Limits of Constructive Security Proofs

OAEP is Secure Under Key-dependent Messages

Type-checking zero-knowledge

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol

Formally Bounding the Side-Channel Leakage in Unknown-Message Attacks

Brief Announcement: Anonymous and Censorship-resistant Content-sharing in Unstructured Overlays

CASPA: Causality-based Abstraction for Security Protocol Analysis

Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus

Key-dependent Message Security under Active Attacks - BRSIM/UC-Soundness of Symbolic Encryption with Key Cycles

Conditional Reactive Simulatability

Limits of the BRSIM/UC soundness of Dolev-Yao-style XOR


Information Flow in the Peer-Reviewing Process (extended abstract)

On the Necessity of Rewinding in Secure Multiparty Computation

Vorgetäuscht / Böse Textdokumente -- Postscript gone wild

On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography

A Calculus of Challenges and Responses

Key-dependent Message Security under Active Attacks - BRSIM/UC-Soundness of Symbolic Encryption with Key Cycles

The Reactive Simulatability Framework for Asynchronous Systems

Enterprise Privacy Policies and Languages

Causality-based Abstraction of Multiplicity in Security Protocols

Causality-based Abstraction of Multiplicity in Security Protocol Analysis

On the Security of Protocols with Logarithmic Communication Complexity

Enterprise Privacy Policies and Languages


Computationally Sound Secrecy Proofs by Mechanized Flow Analysis

Secure Key-Updating for Lazy Revocation

Limits of the Reactive Simulatability/UC of Dolev-Yao Models with Hashes

Conditional Reactive Simulatability

Cryptographically Sound Security Proofs for Basic and Public-key Kerberos

Compositional Analysis of Contract Signing Protocols

Formal Methods and Cryptography

Cryptographically Sound Theorem Proving

On the Cryptographic Key Secrecy of the Strengthened Yahalom Protocol

Real-or-Random Key Secrecy of the Otway-Rees Protocol via a Symbolic Security Proof

Symbolic and Cryptographic Analysis of the Secure WS-ReliableMessaging Scenario

Games and the Impossibility of Realizable Ideal Functionality

Soundness Limits of Dolev-Yao Models

Proceedings of 9th International Conference on Information Security (ISC), Samos Island, Greece

On the Necessity of Rewinding in Secure Multiparty Computation


On Fairness in Simulatability-based Cryptographic Systems

Lazy Revocation in Cryptographic File Systems

Tailoring the Dolev-Yao Abstraction to Web Services Realities - A Comprehensive Wish List

Anonymous yet accountable access control

Unifying Simulatability Definitions in Cryptographic Systems under Different Timing Assumptions

Limits of the Cryptographic Realization of Dolev-Yao-style XOR

Quantifying Probabilistic Information Flow in Computational Reactive Systems

Compositional Analysis of Contract Signing Protocols

A Cryptographically Sound Dolev-Yao Style Security Proof of an Electronic Payment System

Relating Symbolic and Cryptographic Secrecy

Relating Symbolic and Cryptographic Secrecy

Public-Key Steganography with Active Attacks

Symmetric Authentication Within a Simulatable Cryptographic Library

Reactively Secure Signature Schemes

Proceedings of 3rd International Workshop on Security and Concurrency (SecCo), affiliated with CONCUR'05, San Francisco, CA


A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol

A Cryptographically Sound Dolev-Yao Style Security Proof of the Otway-Rees Protocol

Low-level Ideal Signatures and General Integrity Idealization

How to Break and Repair a Universally Composable Signature Functionality

An Algebra for Composing Enterprise Privacy Policies

Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library

Unification in Privacy Policy Evaluation - Translating EPAL to Prolog

Efficient Comparison of Enterprise Privacy Policies

A General Composition Theorem for Secure Reactive System

Computational Probabilistic Non-Interference

Polynomial Liveness

Justifying a Dolev-Yao Model under Active Attacks


A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol

A Composable Cryptographic Library with Nested Operations

A Toolkit for Managing Enterprise Privacy Policies

Symmetric Authentication Within a Simulatable Cryptographic Library

Reactively Secure Signature Schemes

Unifying Simulatability Definitions in Cryptographic Systems under Different Timing Assumptions (Extended Abstract)

From Absence of Certain Vulnerabilities towards Security Proofs - Pushing the Limits of Formal Verification

Proactive Secure Message Transmission in Asynchronous Networks

Security in Business Process Engineering

Reliable broadcast in a computational hybrid model with Byzantine faults, crashes, and recoveries

Intransitive Non-Interference for Cryptographic Purposes

Cryptographically Sound and Machine-Assisted Verification of Security Protocols

A Cryptographically Sound Security Proof of the Needham-Schroeder-Lowe Public-Key Protocol (Extended Abstract)

Proceedings of 1st ACM Workshop on Formal Methods in Security Engineering (FMSE) , affiliated with ACM CCS'03, Washington D.C.


Computational Probabilistic Non-Interference

Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation

Polynomial Fairness and Liveness

Cryptographically Sound Analysis of Security Protocols

New Number-Theoretic Assumptions in Cryptography (in german)

Factorization of Univariate Polynomials