Skip to main content

From probabilistic operational semantics to information theory — side channels with pGCL in isabelle


David Cock




In this paper, we formally derive the probabilistic security predicate (expectation) for a guessing attack against a system with side-channel leakage, modelled in pGCL. Our principal theoretical contribution is to link the process-oriented view, where attacker and system execute particular model programs, and the information-theoretic view, where the attacker solves an optimal-decoding problem, viewing the system as a noisy channel. Our practical contribution is to illustrate the selection of probabilistic loop invariants to verify such security properties, and the demonstration of a mechanical proof linking traditionally distinct domains.

BibTeX Entry

    publisher        = {Springer},
    booktitle        = {Proceedings of the 5th International Conference on Interactive Theorem Proving},
    month            = jul,
    paperurl         = {},
    slides           = {},
    year             = {2014},
    keywords         = {pgcl isabelle security},
    title            = {From Probabilistic Operational Semantics to Information Theory --- Side Channels with {pGCL} in
    pages            = {1--15},
    author           = {Cock, David},
    address          = {Vienna, Austria}