Specifying and verifying organizational security properties in first-order logic

DOI10.1007/978-3-642-17172-7_3MaRDI QIDQ3058451zbMATH OpenOpenAlexFDO

Authors Christoph Brandt, Jens Otten, Christoph Kreitz, Wolfgang Bibel

Publication date 22 November 2010

Published in Verification, Induction, Termination Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-17172-7_3

zbMATH Keywords

securitytheorem proving\textsf{leanCoP}Bell-La PadulaChinese Wallfirst-order-logicorganizational data-flow

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of organizations, manpower planning in operations research (90B70)

Recommendations

• scientific article; zbMATH DE number 1090100
• Formal specification and validation of security policies
• An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
• scientific article; zbMATH DE number 1836549
• Specifying and verifying secrecy in workflows with arbitrarily many agents

Cites work

• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 1543301 (Why is no real title available?)
• Abstract behavior types: a foundation model for components and their composition
• An Efficient Unification Algorithm
• Analyzing rule sets for the calculation of banking fees by a theorem prover with constraints
• Connections in nonclassical logics
• IeanCOP: lean connection-based theorem proving
• Matings in matrices
• Model elimination and connection tableau procedures
• Restricting backtracking in connection calculi
• SETHEO: A high-performance theorem prover
• The CADE-22 automated theorem proving system competition -- CASC-22
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions)

Describes a project that uses

Uses Software

• KoMeT
• ileanCoP
• leanCoP
• TPTP
• SETHEO

This page was built for publication: Specifying and verifying organizational security properties in first-order logic

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