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.
A cut-off theorem is obtained: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size, so secrecy also reduces to a coverability problem in WSTS.
Ioana Boureanu, R. Ramanujam, Srinibas Swain· 0 citations
We introduce a keyless coding/cryptographic primitive that asks for two guarantees at once: the receiver is never fooled into accepting a message other than the one sent, and the adversary learns nothing about the message unless the receiver aborts. Neither the sender nor the receiver holds a secret key, and no computa...
Anne Broadbent, Upendra S. Kapshikar, Denis Rochette· 0 citations
This work builds the flow-sensitive type system family that the quantale calls for, and shows that the object which makes such families useful, the universal type object from which every member specialises, splits in two, with a consequence for enforcement.
A rational Dolev--Yao attacker is introduced, a DY intruder whose actions carry costs and whose security-violating goals carry rewards, and a protocol is called rationally secure when no intruder strategy achieves a violation with strictly positive utility, expressed in a weighted fragment of ATL (WATL).
Trusted Execution Environments (TEEs) provide hardware-supported isolation through enclaves that protect code and data independently of software abstractions. However, TEEs alone cannot enforce information-flow security. This problem is further aggravated in LLVM-like low-level languages that allow unrestricted pointer...
Wesley B. Nuzzo, Samuel Dodson, Benjamin Houle et al.· 0 citations
It is shown that non-trivial PoS follow from (a) $\mathsf{E}=\mathsf{DTIME[2^{O(n)}]}$ is hard for exponential-size nondeterministic circuits, and (b) collision-resistant hash functions, and (c) SNARGs for $\mathsf{P}$.
