Dolev-Yao Information Flow
We propose a variant of classic information flow analysis that permits transmission of secrets over a public network, provided that secrets are suitably encrypted. In the style of Dolev and Yao, the intruder controls the network, observing all messages sent, but can only decrypt messages for which they know the decryption key, i.e., those keys which correspond to the security level of the intruder. In contrast to similar previous works we allow the intruder to send arbitrary bit strings as input to the program without any assumption that these inputs are in some sense well-typed. This means that cryptographic messages can enter program variables that were not meant to hold cryptographic messages and become part of computations and conditions. Despite this strong intruder model, we show that a program that satisfies our information-flow analysis also enjoys Dolev-Yao noninterference, a variant of standard noninterference where the intruder cannot break cryptography. The underlying model, which combines operating on actual bit strings with a symbolic intruder model, and the entire result are formalized and proved in Isabelle/HOL.