Model checking the observational determinism security property using PROMELA and SPIN

DOI10.1007/S00165-014-0331-XzbMATH Open1347.68222OpenAlexW1966189394MaRDI QIDQ903490FDOQ903490

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

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

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)

Cites Work

• Logic in Computer Science
• Title not available (Why is that?)
• A lattice model of secure information flow
• Model Checking on Trees with Path Equivalences
• Static Analysis
• Model Checking Information Flow in Reactive Systems

Cited In (1)

• Model-Checking Helena Ensembles with Spin

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)