@CONFERENCE\{IMM2004-03248,
    author       = "M. Buchholtz and S. Gilmore and J. Hillston and F. Nielson",
    title        = "Securing statically-verified communications protocols against timing attacks",
    year         = "2004",
    booktitle    = "Proceedings of First International Workshop on Practical Applications of Stochastic Modelling ({PASM} 04)",
    volume       = "",
    series       = "Electronic Notes in Computer Science",
    editor       = "",
    publisher    = "",
    organization = "",
    address      = "",
    note         = "To appear.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/3248-full.html",
    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 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."
}