Quantitative information flow as safety and liveness hyperproperties

DOI10.1016/j.tcs.2013.07.031zbMath1359.68201arXiv1207.0871OpenAlexW2963472894MaRDI QIDQ2453117

Tachio Terauchi, Hirotoshi Yasuoka

Publication date: 6 June 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1207.0871

zbMATH Keywords

verificationquantitative information flowhyperproperties

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Hybrid statistical estimation of mutual information and its application to information flow ⋮ Quantitative information flow as safety and liveness hyperproperties ⋮ Secure Multi-party Computation: Information Flow of Outputs and Game Theory ⋮ Quantifying information leakage of randomized protocols

Cites Work

• Unnamed Item
• Unnamed Item
• A Mathematical Theory of Communication
• Efficient weakest preconditions
• Domain theory in logical form
• Quantitative information flow as safety and liveness hyperproperties
• Quantitative Notions of Leakage for One-try Attacks
• Assessing security threats of looping constructs
• Computing the Leakage of Information-Hiding Systems
• On the Foundations of Quantitative Information Flow
• Avoiding exponential explosion
• Static Analysis