Specifying and Verifying Organizational Security Properties in First-Order Logic

DOI10.1007/978-3-642-17172-7_3zbMath1309.68167OpenAlexW1500978174MaRDI QIDQ3058451

Wolfgang Bibel, Jens Otten, Christoph Kreitz, Christoph Brandt

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

theorem provingsecurity\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)

Uses Software

• Unnamed Item
• TPTP
• leanCoP
• ileanCoP
• KoMeT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• SETHEO: A high-performance theorem prover
• IeanCOP: lean connection-based theorem proving
• Abstract behavior types: a foundation model for components and their composition
• 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)
• The CADE-22 automated theorem proving system competition – CASC-22
• Restricting backtracking in connection calculi
• Matings in matrices
• An Efficient Unification Algorithm

This page was built for publication: Specifying and Verifying Organizational Security Properties in First-Order Logic