ANR Project

TECAP

TECAP: Protocol Analysis - Combining Existing Tools

ANR-17-CE39-0004-01

Journals

• [CDDK222]
  V. Cortier, S. Delaune, J. Dreier and E. Klein. Automatic generation of sources lemmas in TAMARIN: towards automatic proofs of security protocols. Journal of Computer Security , 2022. Bibtex
• [JK21]
  C. Jacomme and S. Kremer. An Extensive Formal Analysis of Multi-factor Authentication Protocols. {ACM} Trans. Priv. Secur. , 2021. Bibtex
• [CDS21]
  V. Cortier, S. Delaune and V. Sundararajan. A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties. J. Autom. Reason. , 2021. Bibtex
• [K21]
  A. Koutsos. Decidability of a Sound Set of Inference Rules for Computational Indistinguishability. ACM Trans. Comput. Log. , 2021. Bibtex
• [CCDD20]
  R. Chrétien, V. Cortier, A. Dallon and S. Delaune. Typing Messages for Free in Security Protocols. ACM Trans. Comput. Log , 2020. Bibtex
• [BCK20]
  K. Babel, V. Cheval and S. Kremer. On the semantics of communications when verifying equivalence properties. J. Comput. Secur. , 2020. Bibtex

Conferences

• [BCW22]
  K. Bhargavan, V. Cheval and C. Wood. A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello. In Proceedings of the 29th ACM Conference on Computer and Communications Security (CCS'22) ACM Press, 2022. Bibtex
• [CCK22]
  V. Cheval, R. Crubillé and S. Kremer. Symbolic protocol verification with dice: process equivalences in the presence of probabilities. In Proceedings of the 35nd IEEE Computer Security Foundations Symposium (CSF'22) IEEE Computer Society, 2022. Bibtex
• [CJKK22]
  V. Cheval, C. Jacomme, S. Kremer and R. Kunnemann. Sapic+: protocol verifiers of the world, unite!. In Proceedings of the 27th 31th USENIX Security Symposium, USENIX Security 2022 (USENIX'22) USENIX Association, 2022. Bibtex
• [DL22]
  S. Delaune and J. Lallemand. One Vote Is Enough for Analysing Privacy. In Proceedings of the 27th European Symposium on Research in Computer Security (ESORICS'22) Lecture Notes in Computer Science, 2022. Bibtex
• [CDD22]
  V. Cortier, A. Dallon and S. Delaune. A small bound on the number of sessions for security protocols. In Proceedings of the 35nd IEEE Computer Security Foundations Symposium (CSF'22) IEEE Computer Society, 2022. Bibtex
• [BDKM22]
  D. Baelde, S. Delaune, A. Koutsos and S. Moreau. Cracking the Stateful Nut — Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. In Proceedings of the 35nd IEEE Computer Security Foundations Symposium (CSF'22) IEEE Computer Society, 2022. Bibtex
• [BCC22]
  B. Blanchet, V. Cheval and V. Cortier. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In Proceedings of the 43nd IEEE Symposium on Security and Privacy (SP'22) IEEE Computer Society, 2022. Bibtex
• [BDJKM21]
  D. Baelde, S. Delaune, C.Jacomme, A. Koutsos and S. Moreau. An Interactive Prover for Protocol Verification in the Computational Model. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (SP'21) IEEE Computer Society, 2021. Bibtex
• [BBBBC21]
  M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao and B. Parno. SoK: Computer-Aided Cryptography. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (SP'21) IEEE Computer Society, 2021. Bibtex
• [BBHKS21]
  M. Barbosa, G. Barthe, B. Grégoire, A. Koutsos and P-Y. Strub. Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS'21) ACM, 2021. Bibtex
• [ABHKL21]
  J. Alwen, B. Blanchet, E. Hauck, E. Kiltz, B. Lipp and D. Riepel. Analysing the HPKE Standard. In Proceedings of the 40th Annual International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT'21) Springer, 2021. Bibtex
• [BDM20]
  D. Baelde, S. Delaune and S. Moreau. A Method for Proving Unlinkability of Stateful Protocols. In Proceedings of the 33nd IEEE Computer Security Foundations Symposium (CSF'20) IEEE Computer Society, 2020. Bibtex
• [CJS20]
  H. Comon, C. Jacomme and G. Scerri. Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. In Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security (CCS'20) ACM, 2020. Bibtex
• [CKR20]
  V. Cheval, S. Kremer and I. Rakotonirina. The Hitchhiker's Guide to Decidability and Complexity of Equivalence Properties in Security Protocols. In Logic, Language, and Security - Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday Springer, 2020. Bibtex
• [CDD20]
  V. Cortier, S. Delaune and J. Dreier. Automatic Generation of Sources Lemmas in Tamarin: Towards Automatic Proofs of Security Protocols. In Proceedings of the 25th European Symposium on Research in Computer Security (ESORICS'20) Springer, 2020. Bibtex
• [BGJKS19]
  G. Barthe, B. Grégoire, C. Jacomme, S. Kremer and P-Y. Strub. Symbolic Methods in Computational Cryptography Proofs. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19) IEEE Computer Society, 2019. Bibtex
• [K19a]
  A. Koutsos. Decidability of a Sound Set of Inference Rules for Computational Indistinguishability. In Proceedings of the 32nd IEEE Computer Security Foundations Symposium (CSF'19) IEEE Computer Society, 2019. Bibtex
• [ABBB19]
  J.B. Almeida, C. Baritel-Ruet, M. Barbosa, G. Barthe, F. Dupressoir, B. Grégoire, V. Laporte, T. Oliveira, A. Stoughton and P-Y. Strub. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS'19) ACM, 2019. Bibtex
• [CKR19]
  V. Cheval, S. Kremer and I. Rakotonirina. Exploiting Symmetries When Proving Equivalence Properties for Security Protocols. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS'19) ACM, 2019. Bibtex
• [K19b]
  A. Koutsos. The 5G-AKA Authentication Protocol Privacy. In Proceedings of the 2019 IEEE European Symposium on Security and Privacy (EuroSP'19) IEEE Computer Society, 2019. Bibtex
• [LBB19]
  B. Lipp, B. Blanchet and K. Bhargavan. A Mechanised Cryptographic Proof of the WireGuard Virtual Private Network Protocol. In Proceedings of the 2019 IEEE European Symposium on Security and Privacy (EuroSP'19) IEEE Computer Society, 2019. Bibtex
• [BDH18]
  D. Baelde, S. Delaune and L. Hirschi. POR for Security Protocol Equivalences - Beyond Action-Determinism. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18) Springer, 2018. Bibtex
• [CDD18]
  V. Cortier, A. Dallon and S. Delaune. Efficiently Deciding Equivalence for Standard Primitives and Phases. In Proceedings of the 23rd European Symposium on Research in Computer Security (ESORICS'18) Springer, 2018. Bibtex
• [D18]
  S. Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD'18) Schloss Dagstuhl, 2018. Bibtex
• [CCT18]
  V. Cheval, V. Cortier and M. Turuani. A Little More Conversation, a Little Less Action, a Lot More Satisfaction: Global States in ProVerif. In Proceedings of the 31th IEEE Computer Security Foundations Symposium (CSF'18) IEEE Computer Society, 2018. Bibtex
• [JK18]
  C. Jacomme and S. Kremer. An Extensive Formal Analysis of Multi-factor Authentication Protocols. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18) IEEE Computer Society, 2018. Bibtex
• [CKR18a]
  V. Cheval, S. Kremer and I. Rakotonirina. DEEPSEC: Deciding Equivalence Properties in Security Protocols - Theory and Practice. In Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P'18) IEEE Computer Society Press, 2018. Bibtex
• [CKR18b]
  V. Cheval, S. Kremer and I. Rakotonirina. The DEEPSEC Prover. In Proceedings of the 30th International Conference on Computer Aided Verification (CAV'18) Springer, 2018. Bibtex
• [B18]
  B. Blanchet. Composition Theorems for CryptoVerif and Application to TLS 1.3. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18) IEEE Computer Society, 2018. Bibtex

Workshop

• [B22]
  B. Blanchet. The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm. In Proceedings of the 9th Workshop on Horn Clauses for Verification and Synthesis IEEE Computer Society, 2022. 2022. Bibtex