Securing Statically-verified Communications Protocols Against Timing Attacks

Mikael Buchholtz, Stephen Gilmore, Jane Hillston, Flemming Nielson

Research output: Contribution to journalArticlepeer-review

Abstract

We present a federated analysis of communication protocols which considers both security properties and timing. These are not entirely independent observations of a protocol; by using timing observations of an executing protocol it is possible to calculate encryption keys which were intended to be secret or to deduce derived information about the nature of the communication even in the presence of unbreakable encryption. Our analysis is based on expressing the protocol as a high-level model and deriving from this process calculus models analysable by the Imperial PEPA Compiler and the LySatool.
Original languageEnglish
Pages (from-to)123-143
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume128
Issue number4
DOIs
Publication statusPublished - 2005

Fingerprint

Dive into the research topics of 'Securing Statically-verified Communications Protocols Against Timing Attacks'. Together they form a unique fingerprint.

Cite this