Skip to main content
CSIRO Logo Data 61 logo

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

Authors

David Cock

NICTA

UNSW

Abstract

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

  @inproceedings{Cock_14,
    publisher        = {Springer},
    booktitle        = {Proceedings of the 5th International Conference on Interactive Theorem Proving},
    month            = jul,
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/7850.pdf},
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/7850.pdf},
    year             = {2014},
    keywords         = {pgcl isabelle security},
    title            = {From Probabilistic Operational Semantics to Information Theory --- Side Channels with {pGCL} in
                        Isabelle},
    pages            = {1--15},
    author           = {Cock, David},
    address          = {Vienna, Austria}
  }

Download