Automated proof of Bell-LaPadula security properties
type: Item
instance of: scholarly article
title: Automated proof of Bell-LaPadula security properties
author: Maximiliano Cristiá
author: Gianfranco Rossi
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
full work available at URL: https://arxiv.org/abs/2001.10512
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356979
zbMATH Keywords: Bell-LaPadula model
zbMATH Keywords: security
zbMATH Keywords: automated proof
zbMATH Keywords: \(\{log\}\)
zbMATH Keywords: set theory
zbMATH Keywords: binary relations
describes a project that uses: Zenon
describes a project that uses: SETL
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Z
describes a project that uses: seL4
MaRDI profile type: Publication
OpenAlex ID: W3046152566
Wikidata QID: Q125024127
cites work: The B-Book
cites work: System-level non-interference of constant-time cryptography. I: Model
cites work: Verified Indifferentiable Hashing into Elliptic Curves
cites work: Model Checking Security Protocols
cites work: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
cites work: A decision procedure for restricted intensional sets
cites work: A set solver for finite set relation algebra
cites work: Solving quantifier-free first-order constraints over finite sets and binary relations
cites work: Foundational Property-Based Testing
cites work: Abstract state machines, Alloy, B, TLA, VDM, and Z. 4th international conference, ABZ 2014, Toulouse, France, June 2--6, 2014. Proceedings
cites work: Set unification
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Q3741005
cites work: Q3995087
DOI: 10.1007/S10817-020-09577-6
description: scientific article; zbMATH DE number 7356979