Certifying cryptographic protocols by abstract model-checking and proof concretization

Autor:	M. Périn, R. Janvier, Y. Lakhnech
Rok vydání:	2006
Předmět:	Model checking Protocol (science) Cryptographic primitive Programming language Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science (miscellaneous) Process (computing) Cryptographic protocol computer.software_genre Computer security Engineering (miscellaneous) computer
Zdroj:	ACM SIGBED Review. 3:37-57
ISSN:	1551-3688
DOI:	10.1145/1183088.1183094
Popis:	In this paper, we report on our effort in enhancing our model-checker for cryptographic protocols with the ability to automatically generate a deductive proof that the protocol meets its specification. More specifically, we discuss a technique that allows to transform an abstract proof extracted from the model-checker to a proof that can be checked independently of the abstracting and model-checking process.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::4a3884ff66f6a7ee87c0237d53ae4a69 https://doi.org/10.1145/1183088.1183094 Zobrazit plný text záznamu