Refining Key Establishment
Refining Key Establishment
We use renement to systematically develop a family of key establishment protocols using a theorem prover. Our development spans four levels of abstraction: abstract security properties, messageless guard protocols, protocols communicating over channels with security properties, and protocols secure with respect to a Dolev-Yao intruder. The protocols we develop are Needham-Schroeder Shared Key, the core of Kerberos 4 and 5, and Denning Sacco, and include realistic features such as key conrmation, replay caches, and encrypted tickets. Our development highlights that messageless guard protocols provide a fundamental abstraction for bridging the gap between security properties and messagebased protocol descriptions. It also shows that the renement approach presented in [33] can be applied, with minor adaption, to families of key establishment protocols and that it scales to protocols of nontrivial size and complexity.
- ETH Zurich Switzerland
- Institute of Information Security Switzerland
REFINEMENT (SOFTWARE ENGINEERING), DEDUKTION + BEWEISEN VON THEOREMEN (KÜNSTLICHE INTELLIGENZ), KORREKTHEIT (THEORIE DER PROGRAMMIERUNG), DEDUCTION + THEOREM PROVING (ARTIFICIAL INTELLIGENCE), NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); REFINEMENT (SOFTWARE ENGINEERING); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); KORREKTHEIT (THEORIE DER PROGRAMMIERUNG); CORRECTNESS (THEORY OF PROGRAMMING); VERFEINERUNG (SOFTWARE ENGINEERING), Data processing, computer science, NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS), CORRECTNESS (THEORY OF PROGRAMMING), PUBLIC-KEY CRYPTOSYSTEMS (CRYPTOGRAPHY), NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); DEDUCTION + THEOREM PROVING (ARTIFICIAL INTELLIGENCE); DEDUKTION + BEWEISEN VON THEOREMEN (KÜNSTLICHE INTELLIGENZ); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); PUBLIC-KEY CRYPTOSYSTEMS (CRYPTOGRAPHY); ÖFFENTLICHE VERSCHLÜSSELUNGSSYSTEME (KRYPTOGRAPHIE), VERFEINERUNG (SOFTWARE ENGINEERING), ÖFFENTLICHE VERSCHLÜSSELUNGSSYSTEME (KRYPTOGRAPHIE), NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME), info:eu-repo/classification/ddc/510, Mathematics, info:eu-repo/classification/ddc/004
REFINEMENT (SOFTWARE ENGINEERING), DEDUKTION + BEWEISEN VON THEOREMEN (KÜNSTLICHE INTELLIGENZ), KORREKTHEIT (THEORIE DER PROGRAMMIERUNG), DEDUCTION + THEOREM PROVING (ARTIFICIAL INTELLIGENCE), NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); REFINEMENT (SOFTWARE ENGINEERING); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); KORREKTHEIT (THEORIE DER PROGRAMMIERUNG); CORRECTNESS (THEORY OF PROGRAMMING); VERFEINERUNG (SOFTWARE ENGINEERING), Data processing, computer science, NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS), CORRECTNESS (THEORY OF PROGRAMMING), PUBLIC-KEY CRYPTOSYSTEMS (CRYPTOGRAPHY), NETWORK PROTOCOLS + COMMUNICATION PROTOCOLS (COMPUTER SYSTEMS); DEDUCTION + THEOREM PROVING (ARTIFICIAL INTELLIGENCE); DEDUKTION + BEWEISEN VON THEOREMEN (KÜNSTLICHE INTELLIGENZ); NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME); PUBLIC-KEY CRYPTOSYSTEMS (CRYPTOGRAPHY); ÖFFENTLICHE VERSCHLÜSSELUNGSSYSTEME (KRYPTOGRAPHIE), VERFEINERUNG (SOFTWARE ENGINEERING), ÖFFENTLICHE VERSCHLÜSSELUNGSSYSTEME (KRYPTOGRAPHIE), NETZWERKPROTOKOLLE + KOMMUNIKATIONSPROTOKOLLE (COMPUTERSYSTEME), info:eu-repo/classification/ddc/510, Mathematics, info:eu-repo/classification/ddc/004
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).8 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!