Security invariants in discrete transition systems

DOI10.1007/S00165-012-0256-1MaRDI QIDQ1941889zbMATH OpenOpenAlexFDO

Authors Thai Son Hoang

Publication date 22 March 2013

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://doc.rero.ch/record/317549/files/165_2012_Article_256.pdf

zbMATH Keywords

invariantsrefinementEvent-Bnoninterference securityshadow semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Recommendations

• Abstractions of non-interference security: probabilistic versus possibilistic
• Compositional noninterference from first principles
• A comparison of semantic models for noninterference
• On intransitive non-interference in some models of concurrency
• Non-interference through determinism

Cites work

• scientific article; zbMATH DE number 194539 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 5051652 (Why is no real title available?)
• Abstractions of non-interference security: probabilistic versus possibilistic
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• Modeling in Event B. System and software engineering.
• The B-Book
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• The shadow knows: refinement and security in sequential programs
• Two Applications of Epistemic Logic in Computer Security

Cited in

(3)

• Abstractions of non-interference security: probabilistic versus possibilistic
• On the security of stepwise triangular systems
• Optimal Secret Protections in Discrete-Event Systems

Describes a project that uses

Uses Software

• Rodin
• ProB
• UNITY

This page was built for publication: Security invariants in discrete transition systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1941889)