Secure information flow by self-composition G Barthe, P D'Argenio, T Rezk 17th IEEE Computer Security Foundations Workshop, 2004, 100-114, 2004 | 475* | 2004 |

Formal certification of code-based cryptographic proofs G Barthe, B Grégoire, S Zanella Béguelin Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2009 | 339 | 2009 |

Computer-aided security proofs for the working cryptographer G Barthe, B Grégoire, S Heraud, SZ Béguelin Annual Cryptology Conference, 71-90, 2011 | 269 | 2011 |

Probabilistic relational reasoning for differential privacy G Barthe, B Köpf, F Olmedo, S Zanella Beguelin Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of …, 2012 | 203 | 2012 |

Relational verification using product programs G Barthe, JM Crespo, C Kunz International Symposium on Formal Methods, 200-214, 2011 | 197 | 2011 |

Verifying constant-time implementations JB Almeida, M Barbosa, G Barthe, F Dupressoir, M Emmi 25th {USENIX} Security Symposium ({USENIX} Security 16), 53-70, 2016 | 166 | 2016 |

Strong non-interference and type-directed higher-order masking G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, PY Strub, ... Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications …, 2016 | 134* | 2016 |

Type-based termination of recursive definitions GJD Barthe, MJ Frade, E Giménez, LF Pinto, T Uustalu Cambridge University Press, 2004 | 131 | 2004 |

A certified lightweight non-interference Java bytecode verifier^{†}G Barthe, D Pichardie, T Rezk Mathematical Structures in Computer Science 23 (5), 1032-1081, 2013 | 128* | 2013 |

*EasyCrypt*: A TutorialG Barthe, F Dupressoir, B Grégoire, C Kunz, B Schmidt, PY Strub Foundations of security analysis and design vii, 146-166, 2013 | 122 | 2013 |

Verified proofs of higher-order masking G Barthe, S Belaïd, F Dupressoir, PA Fouque, B Grégoire, PY Strub Annual International Conference on the Theory and Applications of …, 2015 | 120 | 2015 |

Setoids in type theory G Barthe, V Capretta, O Pons Journal of Functional Programming 13 (2), 261, 2003 | 106 | 2003 |

System-level non-interference for constant-time cryptography G Barthe, G Betarte, J Campo, C Luna, D Pichardie Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications …, 2014 | 101 | 2014 |

Probabilistic relational verification for cryptographic implementations G Barthe, C Fournet, B Grégoire, PY Strub, N Swamy, S Zanella-Béguelin ACM SIGPLAN Notices 49 (1), 193-205, 2014 | 99 | 2014 |

Non-interference for a JVM-like language G Barthe, T Rezk Proceedings of the 2005 ACM SIGPLAN international workshop on Types in …, 2005 | 97 | 2005 |

Pure patterns type systems G Barthe, H Cirstea, C Kirchner, L Liquori ACM SIGPLAN Notices 38 (1), 250-261, 2003 | 97 | 2003 |

Security types preserving compilation G Barthe, A Basu, T Rezk International Workshop on Verification, Model Checking, and Abstract …, 2004 | 85 | 2004 |

Parallel implementations of masking schemes and the bounded moment leakage model G Barthe, F Dupressoir, S Faust, B Grégoire, FX Standaert, PY Strub Annual International Conference on the Theory and Applications of …, 2017 | 83 | 2017 |

Information-theoretic bounds for differentially private mechanisms G Barthe, B Kopf 2011 IEEE 24th Computer Security Foundations Symposium, 191-204, 2011 | 81 | 2011 |

Preventing timing leaks through transactional branching instructions G Barthe, T Rezk, M Warnier Electronic Notes in Theoretical Computer Science 153 (2), 33-55, 2006 | 80 | 2006 |