On integrating confidentiality and functionality in a formal method
DOI10.1007/S00165-013-0285-4zbMATH Open1342.68191OpenAlexW2122718698MaRDI QIDQ736833FDOQ736833
Authors: Michael J. Banks, Jeremy L. Jacob 
Publication date: 5 August 2016
Published in: Formal Aspects of Computing (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s00165-013-0285-4
Recommendations
information flow securityCircusconfidentiality propertiesconfidentiality-preserving refinementmiraclesunifying theories of programming
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55)
Cites Work
- Communication Theory of Secrecy Systems*
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The B-Book
- Unwinding Possibilistic Security Properties
- Protocols for authentification and key establishment
- Title not available (Why is that?)
- A UTP semantics for \textsf{Circus}
- Compositional noninterference from first principles
- A refinement strategy for Circus
- The shadow knows: refinement and security in sequential programs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Preservation of probabilistic information flow under refinement
- The Miracle of Reactive Programming
- Integrated Formal Methods
Cited In (2)
Uses Software
This page was built for publication: On integrating confidentiality and functionality in a formal method
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q736833)
