Processing math: 100%
Email: pierre-yves [at] strub.nu
Software
  • EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs.
  • Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant.
  • Coq Modulo Theory is an extension of the Coq proof assistant embedding, in its computational mechanism, validity entailment for user-defined first-order equational theories.
  • Some of my developments can be found on my github profile.
Download
Publications

The following list of publications has been extracted from my DBLP page.

generated by bibbase.org
  2022 (2)
A drag-and-drop proof tactic. Donato, P.; Strub, P.; and Werner, B. In Popescu, A.; and Zdancewic, S., editor(s), CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 197–209, 2022. ACM
A drag-and-drop proof tactic [link]Paper   doi   link   bibtex   4 downloads  
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. Hülsing, A.; Meijers, M.; and Strub, P. In Dodis, Y.; and Shrimpton, T., editor(s), Advances in Cryptology - CRYPTO 2022 - 42nd Annual International Cryptology Conference, CRYPTO 2022, Santa Barbara, CA, USA, August 15-18, 2022, Proceedings, Part I, volume 13507, of Lecture Notes in Computer Science, pages 622–653, 2022. Springer
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt [link]Paper   doi   link   bibtex  
  2021 (3)
EasyPQC: Verifying Post-Quantum Cryptography. Barbosa, M.; Barthe, G.; Fan, X.; Grégoire, B.; Hung, S.; Katz, J.; Strub, P.; Wu, X.; and Zhou, L. In Kim, Y.; Kim, J.; Vigna, G.; and Shi, E., editor(s), CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, pages 2564–2586, 2021. ACM
EasyPQC: Verifying Post-Quantum Cryptography [link]Paper   doi   link   bibtex   1 download  
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. Barbosa, M.; Barthe, G.; Grégoire, B.; Koutsos, A.; and Strub, P. In Kim, Y.; Kim, J.; Vigna, G.; and Shi, E., editor(s), CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security, Virtual Event, Republic of Korea, November 15 - 19, 2021, pages 2541–2563, 2021. ACM
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability [link]Paper   doi   link   bibtex   1 download  
Unsolvability of the Quintic Formalized in Dependent Type Theory. Bernard, S.; Cohen, C.; Mahboubi, A.; and Strub, P. In Cohen, L.; and Kaliszyk, C., editor(s), 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193, of LIPIcs, pages 8:1–8:18, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Unsolvability of the Quintic Formalized in Dependent Type Theory [link]Paper   doi   link   bibtex  
  2020 (3)
Formalizing the Face Lattice of Polyhedra. Allamigeon, X.; Katz, R. D.; and Strub, P. In Peltier, N.; and Sofronie-Stokkermans, V., editor(s), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167, of Lecture Notes in Computer Science, pages 185–203, 2020. Springer
Formalizing the Face Lattice of Polyhedra [link]Paper   doi   link   bibtex   10 downloads  
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. Almeida, J. B.; Barbosa, M.; Barthe, G.; Grégoire, B.; Koutsos, A.; Laporte, V.; Oliveira, T.; and Strub, P. In 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 2020, pages 965–982, 2020. IEEE
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations [link]Paper   doi   link   bibtex   1 download  
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; Standaert, F.; and Strub, P. J. Cryptogr. Eng., 10(1): 17–26. 2020.
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations [link]Paper   doi   link   bibtex   1 download  
  2019 (4)
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. Almeida, J. B.; Baritel-Ruet, C.; Barbosa, M.; Barthe, G.; Dupressoir, F.; Grégoire, B.; Laporte, V.; Oliveira, T.; Stoughton, A.; and Strub, P. In Cavallaro, L.; Kinder, J.; Wang, X.; and Katz, J., editor(s), Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 1607–1622, 2019. ACM
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3 [link]Paper   doi   link   bibtex   2 downloads  
A Machine-Checked Proof of Security for AWS Key Management Service. Almeida, J. B.; Barbosa, M.; Barthe, G.; Campagna, M.; Cohen, E.; Grégoire, B.; Pereira, V.; Portela, B.; Strub, P.; and Tasiran, S. In Cavallaro, L.; Kinder, J.; Wang, X.; and Katz, J., editor(s), Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 63–78, 2019. ACM
A Machine-Checked Proof of Security for AWS Key Management Service [link]Paper   doi   link   bibtex   2 downloads  
Symbolic Methods in Computational Cryptography Proofs. Barthe, G.; Grégoire, B.; Jacomme, C.; Kremer, S.; and Strub, P. In 32nd IEEE Computer Security Foundations Symposium, CSF 2019, Hoboken, NJ, USA, June 25-28, 2019, pages 136–151, 2019. IEEE
Symbolic Methods in Computational Cryptography Proofs [link]Paper   doi   link   bibtex   3 downloads  
Relational ⋆⋆\star-Liftings for Differential Privacy. Barthe, G.; Espitau, T.; Hsu, J.; Sato, T.; and Strub, P. Log. Methods Comput. Sci., 15(4). 2019.
Relational \(⋆\)\(⋆\)\star-Liftings for Differential Privacy [link]Paper   doi   link   bibtex  
  2018 (4)
Computer-Aided Proofs for Multiparty Computation with Active Security. Haagh, H.; Karbyshev, A.; Oechsner, S.; Spitters, B.; and Strub, P. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 119–131, 2018. IEEE Computer Society
Computer-Aided Proofs for Multiparty Computation with Active Security [link]Paper   doi   link   bibtex   3 downloads  
An Assertion-Based Program Logic for Probabilistic Programs. Barthe, G.; Espitau, T.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P. In Ahmed, A., editor(s), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801, of Lecture Notes in Computer Science, pages 117–144, 2018. Springer
An Assertion-Based Program Logic for Probabilistic Programs [link]Paper   doi   link   bibtex   1 download  
hacspec: Towards Verifiable Crypto Standards. Bhargavan, K.; Kiefer, F.; and Strub, P. In Cremers, C.; and Lehmann, A., editor(s), Security Standardisation Research - 4th International Conference, SSR 2018, Darmstadt, Germany, November 26-27, 2018, Proceedings, volume 11322, of Lecture Notes in Computer Science, pages 1–20, 2018. Springer
hacspec: Towards Verifiable Crypto Standards [link]Paper   doi   link   bibtex  
Proving expected sensitivity of probabilistic programs. Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; and Strub, P. Proc. ACM Program. Lang., 2(POPL): 57:1–57:29. 2018.
Proving expected sensitivity of probabilistic programs [link]Paper   doi   link   bibtex  
  2017 (9)
Jasmin: High-Assurance and High-Speed Cryptography. Almeida, J. B.; Barbosa, M.; Barthe, G.; Blot, A.; Grégoire, B.; Laporte, V.; Oliveira, T.; Pacheco, H.; Schmidt, B.; and Strub, P. In Thuraisingham, B.; Evans, D.; Malkin, T.; and Xu, D., editor(s), Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 1807–1823, 2017. ACM
Jasmin: High-Assurance and High-Speed Cryptography [link]Paper   doi   link   bibtex   1 download  
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. Barthe, G.; Dupressoir, F.; Faust, S.; Grégoire, B.; Standaert, F.; and Strub, P. In Coron, J.; and Nielsen, J. B., editor(s), Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30 - May 4, 2017, Proceedings, Part I, volume 10210, of Lecture Notes in Computer Science, pages 535–566, 2017.
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model [link]Paper   doi   link   bibtex  
*-Liftings for Differential Privacy. Barthe, G.; Espitau, T.; Hsu, J.; Sato, T.; and Strub, P. In Chatzigiannakis, I.; Indyk, P.; Kuhn, F.; and Muscholl, A., editor(s), 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80, of LIPIcs, pages 102:1–102:12, 2017. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
*-Liftings for Differential Privacy [link]Paper   doi   link   bibtex  
Proving uniformity and independence by self-composition and coupling. Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; and Strub, P. In Eiter, T.; and Sands, D., editor(s), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46, of EPiC Series in Computing, pages 385–403, 2017. EasyChair
Proving uniformity and independence by self-composition and coupling [link]Paper   doi   link   bibtex  
Coq without Type Casts: A Complete Proof of Coq Modulo Theory. Jouannaud, J.; and Strub, P. In Eiter, T.; and Sands, D., editor(s), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46, of EPiC Series in Computing, pages 474–489, 2017. EasyChair
Coq without Type Casts: A Complete Proof of Coq Modulo Theory [link]Paper   doi   link   bibtex   2 downloads  
Coupling proofs are probabilistic product programs. Barthe, G.; Grégoire, B.; Hsu, J.; and Strub, P. In Castagna, G.; and Gordon, A. D., editor(s), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 161–174, 2017. ACM
Coupling proofs are probabilistic product programs [link]Paper   doi   link   bibtex  
Machine-Checked Proofs of Privacy for Electronic Voting Protocols. Cortier, V.; Dragan, C. C.; Dupressoir, F.; Schmidt, B.; Strub, P.; and Warinschi, B. In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pages 993–1008, 2017. IEEE Computer Society
Machine-Checked Proofs of Privacy for Electronic Voting Protocols [link]Paper   doi   link   bibtex  
A messy state of the union: taming the composite state machines of TLS. Beurdouche, B.; Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Zinzindohoue, J. K. Commun. ACM, 60(2): 99–107. 2017.
A messy state of the union: taming the composite state machines of TLS [link]Paper   doi   link   bibtex  
A relational logic for higher-order programs. Aguirre, A.; Barthe, G.; Gaboardi, M.; Garg, D.; and Strub, P. Proc. ACM Program. Lang., 1(ICFP): 21:1–21:29. 2017.
A relational logic for higher-order programs [link]Paper   doi   link   bibtex   2 downloads  
  2016 (8)
Strong Non-Interference and Type-Directed Higher-Order Masking. Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; Strub, P.; and Zucchini, R. In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 116–129, 2016. ACM
Strong Non-Interference and Type-Directed Higher-Order Masking [link]Paper   doi   link   bibtex   1 download  
Differentially Private Bayesian Programming. Barthe, G.; Farina, G. P.; Gaboardi, M.; Arias, E. J. G.; Gordon, A.; Hsu, J.; and Strub, P. In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 68–79, 2016. ACM
Differentially Private Bayesian Programming [link]Paper   doi   link   bibtex  
Advanced Probabilistic Couplings for Differential Privacy. Barthe, G.; Fong, N.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P. In Weippl, E. R.; Katzenbeisser, S.; Kruegel, C.; Myers, A. C.; and Halevi, S., editor(s), Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016, pages 55–67, 2016. ACM
Advanced Probabilistic Couplings for Differential Privacy [link]Paper   doi   link   bibtex  
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. Bernard, S.; Bertot, Y.; Rideau, L.; and Strub, P. In Avigad, J.; and Chlipala, A., editor(s), Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016, pages 76–87, 2016. ACM
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials [link]Paper   Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials [pdf] link   doi   link   bibtex  
A Program Logic for Union Bounds. Barthe, G.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P. In Chatzigiannakis, I.; Mitzenmacher, M.; Rabani, Y.; and Sangiorgi, D., editor(s), 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55, of LIPIcs, pages 107:1–107:15, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik
A Program Logic for Union Bounds [link]Paper   A Program Logic for Union Bounds [pdf] link   doi   link   bibtex  
Proving Differential Privacy via Probabilistic Couplings. Barthe, G.; Gaboardi, M.; Grégoire, B.; Hsu, J.; and Strub, P. In Grohe, M.; Koskinen, E.; and Shankar, N., editor(s), Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 749–758, 2016. ACM
Proving Differential Privacy via Probabilistic Couplings [link]Paper   doi   link   bibtex  
Dependent types and multi-monadic effects in F. Swamy, N.; Hritcu, C.; Keller, C.; Rastogi, A.; Delignat-Lavaud, A.; Forest, S.; Bhargavan, K.; Fournet, C.; Strub, P.; Kohlweiss, M.; Zinzindohoue, J. K.; and Béguelin, S. Z. In Bodík, R.; and Majumdar, R., editor(s), Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 256–270, 2016. ACM
Dependent types and multi-monadic effects in F [link]Paper   Dependent types and multi-monadic effects in F [pdf] link   doi   link   bibtex   1 download  
Computer-Aided Verification for Mechanism Design. Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Roth, A.; and Strub, P. In Cai, Y.; and Vetta, A., editor(s), Web and Internet Economics - 12th International Conference, WINE 2016, Montreal, Canada, December 11-14, 2016, Proceedings, volume 10123, of Lecture Notes in Computer Science, pages 279–293, 2016. Springer
Computer-Aided Verification for Mechanism Design [link]Paper   doi   link   bibtex  
  2015 (4)
Verified Proofs of Higher-Order Masking. Barthe, G.; Belaïd, S.; Dupressoir, F.; Fouque, P.; Grégoire, B.; and Strub, P. In Oswald, E.; and Fischlin, M., editor(s), Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part I, volume 9056, of Lecture Notes in Computer Science, pages 457–485, 2015. Springer
Verified Proofs of Higher-Order Masking [link]Paper   doi   link   bibtex  
Relational Reasoning via Probabilistic Coupling. Barthe, G.; Espitau, T.; Grégoire, B.; Hsu, J.; Stefanesco, L.; and Strub, P. In Davis, M.; Fehnker, A.; McIver, A.; and Voronkov, A., editor(s), Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450, of Lecture Notes in Computer Science, pages 387–401, 2015. Springer
Relational Reasoning via Probabilistic Coupling [link]Paper   doi   link   bibtex  
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Roth, A.; and Strub, P. In Rajamani, S. K.; and Walker, D., editor(s), Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55–68, 2015. ACM
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy [link]Paper   doi   link   bibtex  
A Messy State of the Union: Taming the Composite State Machines of TLS. Beurdouche, B.; Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Zinzindohoue, J. K. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015, pages 535–552, 2015. IEEE Computer Society
A Messy State of the Union: Taming the Composite State Machines of TLS [link]Paper   doi   link   bibtex  
  2014 (7)
Proving the TLS Handshake Secure (As It Is). Bhargavan, K.; Fournet, C.; Kohlweiss, M.; Pironti, A.; Strub, P.; and Béguelin, S. Z. In Garay, J. A.; and Gennaro, R., editor(s), Advances in Cryptology - CRYPTO 2014 - 34th Annual Cryptology Conference, Santa Barbara, CA, USA, August 17-21, 2014, Proceedings, Part II, volume 8617, of Lecture Notes in Computer Science, pages 235–255, 2014. Springer
Proving the TLS Handshake Secure (As It Is) [link]Paper   doi   link   bibtex  
Certified Synthesis of Efficient Batch Verifiers. Akinyele, J. A.; Barthe, G.; Grégoire, B.; Schmidt, B.; and Strub, P. In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pages 153–165, 2014. IEEE Computer Society
Certified Synthesis of Efficient Batch Verifiers [link]Paper   doi   link   bibtex  
Proving Differential Privacy in Hoare Logic. Barthe, G.; Gaboardi, M.; Arias, E. J. G.; Hsu, J.; Kunz, C.; and Strub, P. In IEEE 27th Computer Security Foundations Symposium, CSF 2014, Vienna, Austria, 19-22 July, 2014, pages 411–424, 2014. IEEE Computer Society
Proving Differential Privacy in Hoare Logic [link]Paper   doi   link   bibtex  
A Formal Library for Elliptic Curves in the Coq Proof Assistant. Bartzia, E.; and Strub, P. In Klein, G.; and Gamboa, R., editor(s), Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558, of Lecture Notes in Computer Science, pages 77–92, 2014. Springer
A Formal Library for Elliptic Curves in the Coq Proof Assistant [link]Paper   doi   link   bibtex  
Probabilistic relational verification for cryptographic implementations. Barthe, G.; Fournet, C.; Grégoire, B.; Strub, P.; Swamy, N.; and Béguelin, S. Z. In Jagannathan, S.; and Sewell, P., editor(s), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 193–206, 2014. ACM
Probabilistic relational verification for cryptographic implementations [link]Paper   doi   link   bibtex  
Gradual typing embedded securely in JavaScript. Swamy, N.; Fournet, C.; Rastogi, A.; Bhargavan, K.; Chen, J.; Strub, P.; and Bierman, G. M. In Jagannathan, S.; and Sewell, P., editor(s), The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 425–438, 2014. ACM
Gradual typing embedded securely in JavaScript [link]Paper   doi   link   bibtex  
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. Bhargavan, K.; Delignat-Lavaud, A.; Fournet, C.; Pironti, A.; and Strub, P. In 2014 IEEE Symposium on Security and Privacy, SP 2014, Berkeley, CA, USA, May 18-21, 2014, pages 98–113, 2014. IEEE Computer Society
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS [link]Paper   doi   link   bibtex  
  2013 (4)
EasyCrypt: A Tutorial. Barthe, G.; Dupressoir, F.; Grégoire, B.; Kunz, C.; Schmidt, B.; and Strub, P. In Aldini, A.; López, J.; and Martinelli, F., editor(s), Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures, volume 8604, of Lecture Notes in Computer Science, pages 146–166, 2013. Springer
EasyCrypt: A Tutorial [link]Paper   doi   link   bibtex  
Fully abstract compilation to JavaScript. Fournet, C.; Swamy, N.; Chen, J.; Dagand, P.; Strub, P.; and Livshits, B. In Giacobazzi, R.; and Cousot, R., editor(s), The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 371–384, 2013. ACM
Fully abstract compilation to JavaScript [link]Paper   doi   link   bibtex   1 download  
Implementing TLS with Verified Cryptographic Security. Bhargavan, K.; Fournet, C.; Kohlweiss, M.; Pironti, A.; and Strub, P. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013, pages 445–459, 2013. IEEE Computer Society
Implementing TLS with Verified Cryptographic Security [link]Paper   doi   link   bibtex  
Secure distributed programming with value-dependent types. Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; and Yang, J. J. Funct. Program., 23(4): 402–451. 2013.
Secure distributed programming with value-dependent types [link]Paper   doi   link   bibtex   2 downloads  
  2012 (1)
Self-certification: bootstrapping certified typecheckers in F* with Coq. Strub, P.; Swamy, N.; Fournet, C.; and Chen, J. In Field, J.; and Hicks, M., editor(s), Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 571–584, 2012. ACM
Self-certification: bootstrapping certified typecheckers in F* with Coq [link]Paper   doi   link   bibtex   2 downloads  
  2011 (3)
Modular code-based cryptographic verification. Fournet, C.; Kohlweiss, M.; and Strub, P. In Chen, Y.; Danezis, G.; and Shmatikov, V., editor(s), Proceedings of the 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, Illinois, USA, October 17-21, 2011, pages 341–350, 2011. ACM
Modular code-based cryptographic verification [link]Paper   doi   link   bibtex   1 download  
Secure distributed programming with value-dependent types. Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; and Yang, J. In Chakravarty, M. M. T.; Hu, Z.; and Danvy, O., editor(s), Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 266–278, 2011. ACM
Secure distributed programming with value-dependent types [link]Paper   doi   link   bibtex   1 download  
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. Barras, B.; Jouannaud, J.; Strub, P.; and Wang, Q. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 143–151, 2011. IEEE Computer Society
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory [link]Paper   doi   link   bibtex  
  2010 (1)
Coq Modulo Theory. Strub, P. In Dawar, A.; and Veith, H., editor(s), Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247, of Lecture Notes in Computer Science, pages 529–543, 2010. Springer
Coq Modulo Theory [link]Paper   doi   link   bibtex   1 download  
  2008 (1)
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. Blanqui, F.; Jouannaud, J.; and Strub, P. In Ausiello, G.; Karhumäki, J.; Mauri, G.; and Ong, C. L., editor(s), Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, TC 1, Foundations of Computer Science, September 7-10, 2008, Milano, Italy, volume 273, of IFIP, pages 349–365, 2008. Springer
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures [link]Paper   doi   link   bibtex   1 download  
  2007 (1)
Building Decision Procedures in the Calculus of Inductive Constructions. Blanqui, F.; Jouannaud, J.; and Strub, P. In Duparc, J.; and Henzinger, T. A., editor(s), Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646, of Lecture Notes in Computer Science, pages 328–342, 2007. Springer
Building Decision Procedures in the Calculus of Inductive Constructions [link]Paper   doi   link   bibtex  
  2001 (1)
Color image segmentation based on automatic morphological clustering. Géraud, T.; Strub, P.; and Darbon, J. In Proceedings of the 2001 International Conference on Image Processing, ICIP 2001, Thessaloniki, Greece, October 7-10, 2001, pages 70–73, 2001. IEEE
Color image segmentation based on automatic morphological clustering [link]Paper   doi   link   bibtex   2 downloads