Security invariants in discrete transition systems

DOI10.1007/S00165-012-0256-1zbMath1259.68127OpenAlexW1989004114MaRDI QIDQ1941889

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

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

Uses Software

• Rodin
• ProB
• UNITY

Cites Work

• The shadow knows: refinement and security in sequential programs
• The dining cryptographers problem: Unconditional sender and recipient untraceability
• Abstractions of non-interference security: probabilistic versus possibilistic
• Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
• The Shadow Knows: Refinement of Ignorance in Sequential Programs
• The B-Book
• Two Applications of Epistemic Logic in Computer Security
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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