Hidden-Markov program algebra with iteration

Annabelle McIver, Larissa Meinicke, Carroll Morgan

Research output: Contribution to journalArticlepeer-review

10 Citations (Scopus)


We use hidden Markov models to motivate a quantitative compositional semantics for noninterference-based security with iteration, including a refinement-or 'implements' relation that compares two programs with respect to their information leakage; and we propose a program algebra for source-level reasoning about such programs, in particular as a means of establishing that an 'implementation' program leaks no more than its 'specification' program. This joins two themes: we extend our earlier work, having iteration but only qualitative (Morgan 2009), by making it quantitative; and we extend our earlier quantitative work (McIver et al. 2010) by including iteration. We advocate stepwise refinement and source-level program algebra-both as conceptual reasoning tools and as targets for automated assistance. A selection of algebraic laws is given to support this view in the case of quantitative noninterference; and it is demonstrated on a simple iterated password-guessing attack.

Original languageEnglish
Pages (from-to)320-360
Number of pages41
JournalMathematical Structures in Computer Science
Issue number2
Early online date10 Nov 2014
Publication statusPublished - 19 Feb 2015


Dive into the research topics of 'Hidden-Markov program algebra with iteration'. Together they form a unique fingerprint.

Cite this