Automated proof of Bell-LaPadula security properties

DOI10.1007/s10817-020-09577-6OpenAlexW3046152566WikidataQ125024127 ScholiaQ125024127MaRDI QIDQ2031424

Maximiliano Cristiá, Gianfranco Rossi

Publication date: 9 June 2021

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2001.10512

zbMATH Keywords

securityset theorybinary relationsautomated proof\(\{log\}\)Bell-LaPadula model

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

Automated reasoning with restricted intensional sets ⋮ An automatically verified prototype of the Android permissions system ⋮ A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals ⋮ Unnamed Item ⋮ Unnamed Item ⋮ An automatically verified prototype of the Tokeneer ID station specification

Uses Software

• Coq
• Isabelle/HOL
• Zenon
• Z
• seL4
• SETL

Cites Work

• Unnamed Item
• Unnamed Item
• Isabelle/HOL. A proof assistant for higher-order logic
• A set solver for finite set relation algebra
• Solving quantifier-free first-order constraints over finite sets and binary relations
• A decision procedure for restricted intensional sets
• System-level non-interference of constant-time cryptography. I: Model
• Abstract state machines, Alloy, B, TLA, VDM, and Z. 4th international conference, ABZ 2014, Toulouse, France, June 2--6, 2014. Proceedings
• Verified Indifferentiable Hashing into Elliptic Curves
• Foundational Property-Based Testing
• Model Checking Security Protocols
• Set unification
• Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
• The B-Book

This page was built for publication: Automated proof of Bell-LaPadula security properties