HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve?

Résumé : La thèse de Selinger énonce qu'une preuve de sécurité d'un protocole cryptographique, écrit sous forme de clauses de Horn, est une absence de contradiction. Plus constructivement, il s'agit d'un modèle de l'ensemble de clauses donné. Nous montrons comment trouver automatiquement un tel modèle, comment vérifier automatiquement qu'il s'agit d'un modèle, et comme faire certifier cette vérification par un assistant de preuve tel que Coq, automatiquement. La portée de la méthode dépasse les protocoles cryptographiques, et s'applique à tout problème représentable par des clauses de Horn.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03201265
Contributor : Jean Goubault-Larrecq Connect in order to contact the contributor
Submitted on : Tuesday, June 22, 2021 - 11:35:45 AM
Last modification on : Friday, February 4, 2022 - 4:14:57 AM
Long-term archiving on: : Thursday, September 23, 2021 - 6:01:43 PM

File

coqmc-hal.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03201265, version 1

Citation

Jean Goubault-Larrecq. Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve?. 15èmes Journées Francophones sur les Langages Applicatifs (JFLA'04), Jan 2004, Sainte-Marie-de-Ré, France. pp.1--40. ⟨hal-03201265⟩

Share

Metrics

Record views

34

Files downloads

17