From probabilistic operational semantics to information theory — side channels with pGCL in isabelle
Authors
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} }