The Infon Logic

Infons are pieces of information. In our work DKAL (Distributed Knowledge Authorization Language), we discovered that logic of infons is a conservative extension of intuitionistic logic by means of connectives “p said” and “p put” where p ranges over principals. Here we investigate infon logic and a primal fragment of it. In both cases, we formulate an infon calculus, develop a Kripke-type model theory, prove soundness and completeness, and prove the subformula property that is important for computational complexity. We stratify primal logic by quotation depth. In applications, quotation depth is small. Our most involved technical result is this: The derivability problem for any bounded-depth fragment of primal logic is solvable in linear time. One consequence is that the (ground) derivability problem (whether a given query follows form the given ground hypotheses) for SecPAL is solvable in linear time. SecPAL is a precursor of DKAL and expresses many important access control scenarios.