Tools

• Seq-ACL+
  
  Seq-ACL+ is a decidable theorem prover (written in PROLOG) for the modal access control logic ACL+ presented in
  • V. Genovese and D. Garg
    "New Modalities for Access Control Logics: Permission, Control and Ratification"
    7th International Workshop on Security and Trust Management - STM 2011
  
  Source Files [zip]
  

• ACL-Lean
  
  ACL-Lean is a decidable theorem prover (written in PROLOG) for propositional access control logics with says operator.
  ACL-Lean implements an analytic labelled sequent calculus for conditional access control logics presented in
  • V. Genovese, L. Giordano, V. Gliozzi and G. L. Pozzato
    "A Conditional Constructive Logic for Access Control and its Sequent Calculus"
    20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
  
  Source Files [zip]
  

• delegation2spass
  
  delegstion2spass is a parser (written in SCHEME) which implements a set of complete reduction axioms and translates
  dynamic formulas for a delegation/revocation logic into propositional logic expressed in DFG syntax.
  
  The dynamic logic for delegation and revocation schemes, together with its reduction axioms, has been presented in
  • G. Aucher, S. Barker, G. Boella, v. Genovese and L. van der Torre
    "Dynamics in Delegation and Revocation Schemes: A Logical Approach"
    25th IFIP WG 11.3 Conference on Data and Applications Security and Privacy - DBSEC 2011
  
  Source Files [zip]
  

• macl2spass
  
  macl2spass is a parser (written in SCHEME) from policeis written in modal access control logic (M-ACL) into first-order
  formulas expressed in DFG sytnax.
  The output of macl2spass can be directly used to reason about access control with SPASS theorem prover.
  
  macl2spass is related to the work presented in
  • V. Genovese, D. Rispoli, D. M. Gabbay and L. van der Torre
    "Modal Access Control Logic: Axiomatization, Semantics and FOL Theorem Proving"
    Proceedings of the Fifth Starting AI Researchers' Symposium
  
  Source Files [zip]
  Linux Precompiled Package [zip]
  Windows Precompiled Package [zip]
  


• secommunity
  
  secommunity is tool to define distributed access control policies in DLV. In particular, we provide a client to implement external
  predicates in DLV-Complex with the aim to query remote KBs and a server to handle such queries.
  
  Website [link]
  


• normative neural symbolic simulator
  
  The normative neural symbolic simulator is a software suite which implements the Normative-CILP as in
  • G. Boella, S. Colombo Tosatto, A. d'Avila Garcez, V. Genovese, D. Ienco, and L. van der Torre
    "Neural Symbolic Systems for Normative Agents (Extended Abstract)"
    10th International Conference on Autonomous Agents and Multiagent Systems - AAMAS 2011
    
  
  Source Files [zip]