Model checking the observational determinism security property using PROMELA and SPIN

DOI10.1007/S00165-014-0331-XMaRDI QIDQ903490zbMATH OpenOpenAlexFDO

Authors Maryam Dabaghchian, Mohammad Abdollahi Azgomi

Publication date 6 January 2016

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

Full work available at URL https://doi.org/10.1007/s00165-014-0331-x

zbMATH Keywords

model checkinglinear temporal logicSPINinformation flow securityPROMELAobservational determinism

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification of quantum protocols with a probabilistic model-checker
• Model checking indistinguishability of randomized security protocols
• Modelchecking safety properties in randomized security protocols
• EPR-based bounded model checking at word level
• Security analysis of semi-quantum cryptography protocols by model checking
• scientific article; zbMATH DE number 2087629
• The modeling library of eavesdropping methods in quantum cryptography protocols by model checking
• Run-time verification for observational determinism using dynamic program slicing
• scientific article; zbMATH DE number 1538052

Cites work

• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A lattice model of secure information flow
• Logic in Computer Science
• Model Checking Information Flow in Reactive Systems
• Model Checking on Trees with Path Equivalences
• Static Analysis

Cited in

(1)

• Model-Checking Helena Ensembles with Spin

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Model checking the observational determinism security property using PROMELA and SPIN

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