biblio.bib

@inproceedings{bideduction-to-appear,
  author    = {David Baelde and
               Adrien Koutsos and
               Justine Sauvage},
  title     = {Foundations for Cryptographic Reductions in {CCSA} Logics},
  booktitle = {{CCS}},
  pages     = {to appear},
  publisher = {{ACM}},
  year      = {2024},
  url       = {https://inria.hal.science/hal-04511718}
}

@inproceedings{concrete-security,
author = {David {Baelde} and Caroline Fontaine and Adrien Koutsos and Guillaume Scerri and Th{\'{e}}o Vignon},
booktitle = {{CSF}},
title = {A Probabilistic Logic for Concrete Security},
year = 2024,
issn = {2374-8303},
pages = {324-339},
url = {https://inria.hal.science/hal-04577828},
publisher = {{IEEE}},
}


@inproceedings{BDKJM-sp21,
 author = {Baelde, David and Delaune, Stéphanie and Koutsos, Adrien and  Jacomme,Charlie and Moreau, Solène},
  booktitle =	 {{P}roceedings of the 42nd {IEEE} {Symposium} on {Security}
                  and {Privacy} ({S}\&{P}'21)},
  address =	 {San Francisco, CA, USA},
  publisher =	 {{IEEE} Computer Society Press},
 title = {An {Interactive} {Prover} for {Protocol} {Verification} in the {Computational} {Model}},
 year = {2021},
 url= {https://hal.inria.fr/hal-03172119},
}


@inproceedings{BDKM-csf22,
  title = {{Cracking the Stateful Nut}},
  author = {Baelde, David and Delaune, St{\'e}phanie and Koutsos, Adrien and Moreau, Sol{\`e}ne},
  url = {https://hal.archives-ouvertes.fr/hal-03500056},
  booktitle = {{CSF 2022 - 35th IEEE Computer Security Foundations Symposium}},
  address = {Haifa, Israel},
  year = {2022},
}


@inproceedings{CFJ-sp22,
 author = {Cremers, Cas and Fontaine, Caroline and Jacomme, Charlie},
  booktitle =	 {{P}roceedings of the 43nd {IEEE} {Symposium} on {Security}
                  and {Privacy} ({S}\&{P}'22)},
  address =	 {San Francisco, CA, USA},
  publisher =	 {{IEEE} Computer Society Press},
 title = {A {Logic} and an {Interactive} {Prover} for the {Computational} {Post-Quantum} {Security} of {Protocols}},
 year = {2022},
 url = {https://hal.inria.fr/hal-03620358}
}

@INPROCEEDINGS {BKL23,
author = {D. Baelde and A. Koutsos and J. Lallemand},
booktitle = {2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title = {A Higher-Order Indistinguishability Logic for Cryptographic Reasoning},
year = {2023},
volume = {},
issn = {},
pages = {1-13},
abstract = {The field of cryptographic protocol verification in the computational model aims at obtaining formal security proofs of protocols. To facilitate writing such proofs, which are complex and hard to automate, Bana and Comon have proposed the Computationally Complete Symbolic Attacker (CCSA) approach, which is based on a first-order logic with a probabilistic computational semantics. Later, a meta-logic was built on top of the CCSA logic, to extend it with support for unbounded protocols and effective mechanisation. This meta-logic was then implemented in the SQUIRREL prover.In this paper, we propose a careful re-design of the SQUIRREL logic, providing clean and robust foundations for its future development. We show in this way that the original meta-logic was both needlessly complex and too restrictive. Our new, higher-order logic avoids the indirect definition of the meta-logic on top of the CCSA logic, decouples the logic from the notion of protocol, and supports advanced generic reasoning and non-computable functions. We also equip it with generalised cryptographic rules to reason about corruption. This theoretical work justifies our extension of SQUIRREL with higher-order reasoning, which we illustrate on case studies.},
keywords = {computer science;solid modeling;computational modeling;semantics;writing;solids;probabilistic logic},
doi = {10.1109/LICS56636.2023.10175781},
url = {https://hal.inria.fr/hal-03981949},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {jun}
}


@inproceedings{BC14,
  TITLE = {{A Computationally Complete Symbolic Attacker for Equivalence Properties}},
  AUTHOR = {Bana, Gergei and Comon-Lundh, Hubert},
  URL = {https://hal.inria.fr/hal-01102216},
  BOOKTITLE = {{2014 ACM SIGSAC Conference on Computer and Communications Security}},
  ADDRESS = {Scottsdale, United States},
  PUBLISHER = {{ACM}},
  PAGES = {609-620},
  YEAR = {2014},
  MONTH = Nov,
  DOI = {10.1145/2660267.2660276},
  HAL_ID = {hal-01102216},
  HAL_VERSION = {v1},
}


@inproceedings{BDJKL24,
  TITLE = {{The Squirrel Prover and its Logic}},
  AUTHOR = {Baelde, David and Delaune, St{\'e}phanie and Jacomme, Charlie and Koutsos, Adrien and Lallemand, Joseph},
  URL = {https://inria.hal.science/hal-04579038},
  JOURNAL = {{ACM SIGLOG News}},
  PUBLISHER = {{ACM}},
  VOLUME = {11},
  NUMBER = {2},
  YEAR = {2024},
  MONTH = Apr,
  PDF = {https://inria.hal.science/hal-04579038/file/main.pdf},
  HAL_ID = {hal-04579038},
  HAL_VERSION = {v1},
}