  Cyberlogic is an enabling logical foundation for building and analyzing
digital transactions that involve the exchange of digital forms of evidence. It
is based on an extension of (first-order) intuitionistic predicate logic with
an attestation and a knowledge modality. The key ideas underlying Cyberlogic
are extremely simple, as (1) public keys correspond to authorizations, (2)
transactions are specified as distributed logic programs, and (3) verifiable
evidence is collected by means of distributed proof search. Verifiable
evidence, in particular, are constructed from extra-logical elements such as
signed documents and cryptographic signatures. Despite this conceptual
simplicity of Cyberlogic, central features of authorization policies including
trust, delegation, and revocation of authority are definable. An expressive
temporal-epistemic logic for specifying distributed authorization policies and
protocols is therefore definable in Cyberlogic using a trusted time source. We
describe the distributed execution of Cyberlogic programs based on the
hereditary Harrop fragment in terms of distributed proof search, and we
illustrate some fundamental issues in the distributed construction of
certificates. The main principles of encoding and executing cryptographic
protocols in Cyberlogic are demonstrated. Finally, a functional encryption
scheme is proposed for checking certificates of evidential transactions when
policies are kept private.
