Securing statically-verified communications protocols against timing attacks

Mikael Buchholtz, Stephen Gilmore, Jane Hillston, Flemming Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    170 Downloads (Pure)


    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 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 process algebra model and deriving from this process models analysable by the Imperial PEPA Compiler and the LySatool.
    Original languageEnglish
    Title of host publicationProceedings of First International Workshop on Practical Applications of Stochastic Modelling (PASM 04)
    Publication date2004
    Publication statusPublished - 2004

    Fingerprint Dive into the research topics of 'Securing statically-verified communications protocols against timing attacks'. Together they form a unique fingerprint.

    Cite this