A mechanized logic for secure key escrow protocol verification

Autor:	Sarah Mocas, E. Thomas Schubert
Rok vydání:	1995
Předmět:	Correctness Computer science business.industry Escrow HOL Cryptographic protocol Computer security computer.software_genre Encryption Universal composability ComputingMilieux_COMPUTERSANDSOCIETY business computer Key escrow Theorem Proving System
Zdroj:	Higher Order Logic Theorem Proving and Its Applications ISBN: 9783540602750 TPHOLs
DOI:	10.1007/3-540-60275-5_73
Popis:	Reasoning about key escrow protocols has increasingly become an important issue. The Escrowed Encryption Standard (EES) has been proposed as a US government standard for the encryption of unclassified telecommunications. One unique feature of this system is key escrow. The purpose of key escrow is to allow government access to session keys shared by EES devices. We develop a framework to formally specify and verify the correctness of key escrow protocols that we mechanize within the HOL theorem proving system. Our logic closely follows the logic, SVO, used for analyzing cryptographic protocols which was developed by Syverson and vanOorschot [13]. Using the HOL mechanization of SVO, we formally demonstrate the failure of the EES key escrow system by showing that it does not insure that the escrow agent receives correct information. This was previously shown experimentally [2]. Last, we offer an alternative escrow protocol and demonstrate its correctness.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::3821524db9a5da522667a49ddcbfc328 https://doi.org/10.1007/3-540-60275-5_73 Zobrazit plný text záznamu