*[inlinelist,1]label=(0), itemsep=5pt,

#  Evidential Transactions with Cyberlogic

Harald Ruess
fortiss
Guerickestraße 25
D-80805 München
Phone: (089) 3603522-11
<EMAIL_ADDRESS>
Natarajan Shankar
SRI International
333 Ravenswood Avenue
Menlo Park CA 94025
Phone: (650) 859-5272
<EMAIL_ADDRESS>
(CSL Technical Report SRI-CSL-2023-01 • 11 January, 2023 )

###### Abstract

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.

This research has been supported by the DARPA Automated Rapid Certification Of
Software (ARCOS) project under contract number HR0011043439, National
Institute of Aerospace Award #C21-202017-SRI, and NSF Grant SHF-1817204. Any
opinions, findings, and conclusions or recommendations expressed in this
material are those of the author(s) and do not necessarily reflect the views
of the United States Government, DARPA, NASA, NIA, or NSF.

###### Contents

  1. 1 Introduction
  2. 2 Attestation and Knowledge
  3. 3 Distributed Proof Search
  4. 4 Expressiveness
    1. 4.1 Authorization and Delegation
    2. 4.2 Timed Attestation
    3. 4.3 Revocation of Authority
    4. 4.4 Nonces
    5. 4.5 Distibuted Logic Programs
  5. 5 Cryptographic Protocols
  6. 6 Privacy of Policies
  7. 7 Conclusions
  8. A First Incarnation

"If electronic mail systems are
to replace the existing mail system for business transactions,
signing an electronic message must be possible.
The recipient of a signed message has proof
that the message originated from the sender.
This quality is stronger than mere authentication (…);
the recipient can convince a judge
that the signer sent the message."
(Rivest, Shamir, Adleman [RSA78])

##  Chapter 1 Introduction

We have outsourced to Internet technology all kinds of transactions and social
interactions that previously required the mutual attribution of trust and
responsibility. Many of the entities involved in Internet transactions,
however, are unknown to each other, and there usually is no central authority
that everyone trusts. But then, how can we trust that digital transactions are
being executed "on the Internet" as intended? How can we trust that crucial
information is not being misused or leaked? How can we ensure that we are not
being deceived or otherwise being robbed? How can we assure responsibility and
accountability for actions?

As of now we do not have convincing answers for trustworthy Internet
transactions, even though they are already woven into our very societal
fabric. Recent attempts of alleviating the situation based on voluntary self-
commitment of all stakeholders [BL19] have not been proven themselves to be
effective.

Traditional identity-based trust management is also not applicable to Internet
transactions. In older settings of access control, in particular,
authorization of a request is divided into authentication(’who made the
request?’) and access control (’is the requester authorized to perform the
action?’). But this may be ineffective when the resource owner and requester
are unknown to one another. Because the access control mechanism does not know
the requester directly, it has to use information from third parties who know,
or claim to know, the requester better. But, normally, the authorizer trusts
these third parties only for certain things and only to certain degrees. This
trust and delegation aspect makes Internet transactions different from more
traditional access control [LGF03].

Distributed immutable ledgers such as blockchains allow for digital
transactions with little reliance on trusted third-parties. This lack of
trustworthy parties in blockchains, however, has serious consequences for
performance, scalability, and decentralization [CW18]. In addition,
blockchain-based transactions occur in the context of complex programs, which
are sometimes referred to as smart contracts. As such a smart contract
foregoes trusted third-parties and runs on several computers anonymously, it
constitutes a highly critical program that has to be trusted-by-design
[DGP+21] together with its underlying distributed execution (and miner)
framework. In this way, a large number of vulnerabilities coming from the
execution of the programs in a widely distributed blockchain network are fully
exploitable today [ABC17].111 For instance, the DAO exploit
(http://hackingdistributed.com/2016/06/18/ analysis-of-the-dao-exploit/).

Here, we follow the ’verify, then trust’ paradigm of authorization in open
distributed systems [GS00, BFL96, LGF03], where a requester submits a request,
possibly supported by a set of credentials issued by other parties, to an
authorizer who controls the requested resources. The identity information is
just one kind of credential, and it may be necessary and sufficient for some
applications but not for others. The authorizer then decides whether to
authorize this request by answering the proof-of-compliance question: ’do
these credentials prove that a request complies with my policy?’.

Consider, for example, the process of obtaining a visa, which despite its
conceptual simplicity is often overly tedious and error-prone in real life.
The requester initiates a transaction for obtaining a visa by contacting an
authorized visa-issuing consulate and by providing any number of additional
credentials such as deeds, certified translations, and affidavits as
requested. In the course of authorizing a visa request, the consulate usually
contacts other authorities for additional information and background checks
with, among others, banks, health insurance providers, airlines, and keepers
of no-fly lists. In case these checks are positive, the authorized consulate
may decide to issue a visa, which in our case is just a digital certificate
signed by the private key of the consulate. This certificate attests to the
fact that the consulate has issued the desired visa to the requester. Now,
upon entry, the requester presents her visa certificate, and the border
control agent checks, by decrypting the certificate with the corresponding
public key of the issuing consulate and possibly some additional checks, that
the requester indeed is eligible for entering the country. It is easy to
extrapolate from the above scenario to other uses of digital evidence in
electronic commerce, business and administrative processes, and digital
government. The key observation is that these transactions usually involve the
exchange of various forms of evidence.

Cyberlogic is an enabling foundation for building and analyzing digital
transactions that involve the exchange of evidence [RS03, Ber06]. It builds on
the existing public key infrastructure while noting that the utility of such
an infrastructure depends on a coherent and rigorous semantic foundation.
Without such a foundation, terms like authentication, anonymity, trust, and
certification are not meaningful, and the resulting protocols cannot by
themselves provide the necessary guarantees. The correct functioning of
Cyberlogic is primarily based on the correct specification of Cyberlogic
policies, the correct functioning of the underlying public key infrastructure
and the unbreakability of its ciphers. Therefore, and in sharp contrast to
blockchains, there is no need in Cyberlogic to trust smart contracts and their
distributed execution environment, as the kernel of trust in Cyberlogic is
reduced to cryptographic proof checking.

Cyberlogic allows (1) for expressing transactional policies and protocols of a
distributed system’s interacting actors, called principals in this context,
(2) for the distributed execution of transactions, and (3) for generating
tamper-proof verifiable evidence. Each principal receives queries from other
principles, performs computation and deduction in accordance with their
policies and their current knowledge, and communicates responses and
subqueries to other principals. The policy of the visa processing actor above
might require to subquery, among others, bank and insurance principals for
certifying the requestee’s bank account and insurance status. Furthermore, the
border control agent’s policy might permit entry only after checking that the
presented visa certificate has not been revoked recently. The visa itself is
presented in the form of logical relations such as
$hasVisa("JohnDoe",2022,90)$, which are signed by the private key of an
authorized consulate. Consequently, the validity of the presented evidence can
be checked by the border control agent by decrypting this certificate with the
corresponding public key.

Altogether, Cyberlogic is a logic for evidential transactions built on the
public-key infrastructure. The key ideas underlying Cyberlogic are extremely
simple.

  1. 1.

Private/Public key pairs correspond to authorizations;

  2. 2.

Transactional policies are specified as distributed logic programs;

  3. 3.

Verifiable evidence is constructed by distributed proof search.

In this way, logical statements $\varphi$ are signed by private keys $Prv(K)$
to obtain a digital certificate $c$, so that $c$ is evidence for the claim
that (principal/authority) $K$ attests to $\varphi$. This is verified by
decrypting $c$ with the corresponding public key $Pub(K)$ to see if it yields
$\varphi$. Notice that the fact that authority $K$ attests to some logical
statement does not necessarily imply its logical validity.

Transactional policies and protocols are distributed logic programs that
gather evidence by using both ordinary predicates and digital certificates,
and the execution of distributed logic programs corresponds to distributed
proof search. Execution is triggered by a query which itself may trigger,
based on the local policies and knowledge, any number of subqueries. The
communication between principals therefore involves queries and (partial)
answers to these queries.

In the visa example above, the authorized consulate provides a visa
certificate to the requester, which (or its hash) is signed by private key of
the consulate. Upon entry of the requester, the border control agent verifies
the visa certificate by decrypting the provided certificate with the
corresponding public key. Real world authorization schemes, however, are
considerably more complicated. For instance, the authority of handing out
visas might have be dynamically delegated through a chain of authorizations
by, say, the state department and embassies. Also, authorizations such as
visas may be revoked due to a number of different reasons. This complexity and
dynamicity of distributed policies suggests declarative specifications by
means of an expressive logic.

This exposition is structured as follows. Chapter 2 describes the logical
foundation of Cyberlogic, which is based on an extension of intuitionistc
predicate logic with an attestation modality. Chapter 3 illustrates
distributed proof search in Cyberlogic and the interactive, incremental
construction of certificates based on distributed proof search. Then, in
Chapter 4 we demonstrate the expressive power of Cyberlogic by encoding all-
important policy mechanisms such as authorization and delegation (Section
4.1), timed attestation (Section 4.2), revocation of authorities (Section
4.3), and the generation of fresh, unique numbers (Section 4.4). Distributed
execution for the hereditary Harrop fragment is outlined in Chapter 4.5 and
illustrated, by means of the infamous Needham-Schroeder authentication
protocol in Chapter 5. Communication of tree-like certificates in Cyberlogic
might be avoided using the proposed notions of cryptographic proofs in Chapter
6. We conclude with a comparison of Cyberlogic to most-closely related work in
Chapter 6 and some final remarks in Chapter 7.

#### Disclaimer.

This report should most probably have already been finished long time ago, as
it is largely based on an invited talk "Introducing Cyberlogic" at the High
Confidence Software and Systems conference in Baltimore on April 1, 2003. The
original development of Cyberlogic has been supported by the National Science
Foundation under the grant No. 0208779, and the preparation of this report has
been supported by the Bavarian Ministry of Economics in the context of the
fortiss AI Center. We are revisiting Cyberlogic here due to new and increased
interest on trust management for open and large-scale distributed systems such
as the European GAIA-X initiative and decentralized, automated certification
of software in DARPA’s ARCOS project. In particular, we thank Vivek Nigam for
his constructive comments on a previous version of this paper, and Ulrich
Schöpp for suggesting multi-input functional encryption for ensuring the
secrecy of proof checkers.

##  Chapter 2 Attestation and Knowledge

Cyberlogic is an intuitionistic (first-order) predicate logic [D+00] extended
with an attestation modality. In particular, signatures $\Sigma$ are multi-
sorted, and each sort $S$ has an associated domain $Dom(S)$ of interpretation.
Signatures are assumed to contain a sort $Principal$ with a countably infinite
supply of constant symbols, and there is a countably infinite supply of
logical variables for each sort. Atomic formulas are either $\top$, $\bot$,
relations of the form $p(t_{1},\ldots,t_{n})$ with $p$ a relational symbol in
$\Sigma$ and $t_{i}$, for $i=1,\ldots,n$, correspondingly well-sorted
$\Sigma$-terms with variables. Logic formulas are built up recursively in the
usual way, and include atomic formulas, attestations of the form
${K}\,\rhd\,{\phi}$ with $K$ a constant symbol of sort $Principal$ and $\phi$
a formula, conjunctions $\phi\,\land\,\psi$, disjunctions $\phi\,\lor\,\psi$,
implications $\phi\,\Rightarrow\,\psi$, universal quantification $(\forall
x:S)\,\phi$, where $x$ is a logical variable of sort $S$ in $\Sigma$, and,
similarly, existential quantification $(\exists x:S)\,\phi$. Negation
$\lnot\,{\phi}$ is defined as $\phi\,\Rightarrow\,\bot$ and bi-implication
$\phi\,\Leftrightarrow\,\psi$ stands for
$\phi\,\Rightarrow\,\psi\,\land\,\psi\,\Rightarrow\,\phi$.

Some symbols in $\Sigma$ may be interpreted with respect to a first-order
theory. For example, symbols such as $+$, $=_{Nat}$ are interpreted in the
theory of arithmetic (say, Heyting or Peano). A sentence is a formula $\phi$
without any free variables, that is, all variables are bound by a universal or
existantial quantification. Moreover, substitution in $\phi$ of a free
variable $x$ for a well-sorted term $t$, which does not contain $x$, of the
same sort is denoted by $\Phi[x/t]$.

The attestation modality ${K}\,\rhd\,{\phi}$ expresses the fact that principal
$K$ attests to the statement $\phi$. Attestation is, of course, in the
tradition of the says modality [ABLP93] in access control logics, and its
introduction rules are derived from the says modality in lax logics [FM97,
DP01]; more precisely: $\phi\,\Rightarrow\,{K}\,\rhd\,{\phi}$ and
$(\phi\,\Rightarrow\,{K}\,\rhd\,{\psi})\,\,\Rightarrow\,\,({K}\,\rhd\,{\phi}\,\Rightarrow\,{K}\,\rhd\,{\psi})$
hold for all principals $K$ and for all formulas $\phi$, $\psi$. In
particular, any principal can attest to any valid sentence but not every
sentence a principal attests to is valid; that is,
$({K}\,\rhd\,{\phi})\not\,\Rightarrow\,\phi$ holds for all formulas $\phi$.
Moreover, the attestation modality is absorbing
(${K}\,\rhd\,{{K}\,\rhd\,{\phi}}\,\,\Leftrightarrow\,\,{K}\,\rhd\,{\phi}$) but
not commutative
(${K}\,\rhd\,{{L}\,\rhd\,{\phi}}\not\,\Rightarrow\,{L}\,\rhd\,{{K}\,\rhd\,{\phi}}$.

Reconsidering the visa example, somebody named "John Doe" requests a travel
visa for 14 days in 2022. He initiates his request by issuing the query
${Cons42}\,\rhd\,{visa("JohnDoe",2022,90)}$ to the principal $Cons42$, which
is the authorized visa-issuing consulate. This consulate may choose to
respond, after some further authentication and inquiries about financial
status and potential police records, to this request by attesting that "John
Doe" is eligible for entering the country in 2022 on a tourist visa with a
maximum stay of 90 days. In this case, the consulate Cons42 responds by
attesting ${Cons42}\,\rhd\,{visa("JohnDoe",2022,90)}$. This concludes the
transaction between "John Doe" and the consulate Cons42. Such a response,
however, is only of informative nature, as anybody can make up and present
these kinds of claims. Therefore, upon entry into the country, the border
control does not only need to authenticate "John Doe" but it also needs to
verify his visa status by querying for a corresponding entry in the data base
of the responsible authorities. In an evidential transaction, the authorizer
Cons42 provides verifiable evidence that the requester "John Doe" indeed is
eligible for entry to the country on a tourist visa. In this way, the border
control may directly check this evidence for a visa, and permit after
verifying "John Doe"’s identity, for example by checking his passport, but
without any further consultations to other visa-granting authorities.

Think of this evidence as being represented as a number or a digital
certificate. Also, authorities such as the visa-granting consulate Cons42 have
an associated public-private key pair $(Prv(Cons42),Pub(Cons42))$. In general,
every constant symbol $K$ of sort Principal has an associated key pair
$(Prv(K),Pub(K))$ such that111Syntactic equivalence instead of bi-implication
usually suffices.

<EMAIL_ADDRESS>
In this way, the consulate uses its private key $Prv(Cons42)$ to sign the
relation (or its hash) $usTouristVisa("JohnDoe",2022,90)$ and return this
signature as evidence to the requestee. The border control then verifies the
presented evidence simply by decrypting it using the public key of Cons42. In
general, evidence for an attestation ${K}\,\rhd\,{\varphi}$ is a number $c$
such that $Decr(Pub(K),\,c)$ yields $\varphi$. In this case we also say that
$c$ realizes this attestations, and we write:

<EMAIL_ADDRESS>
Based on the Brouwer-Heyting-Kolmogorov (BHK) explanation of intuitionistic
truth, the notion of realizability is extended in the usual way to all
intuitionistic sentences.

$\displaystyle*$ $\displaystyle:$ $\displaystyle\top$ $\displaystyle(c,d)$
$\displaystyle:$ $\displaystyle(\phi\,\land\,\psi)\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\text{if\leavevmode\nobreak\ }c:\phi\text{\leavevmode\nobreak\
and\leavevmode\nobreak\ }d:\psi$ $\displaystyle inl(c)$ $\displaystyle:$
$\displaystyle(\phi\,\lor\,\psi)\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\text{if\leavevmode\nobreak\ }c:\phi$ $\displaystyle inr(d)$ $\displaystyle:$
$\displaystyle(\phi\,\lor\,\psi)\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\text{if\leavevmode\nobreak\ }d:\psi$ $\displaystyle c$ $\displaystyle:$
$\displaystyle(\phi\,\Rightarrow\,\psi)\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\text{if\leavevmode\nobreak\ whenever\leavevmode\nobreak\
~}d:\phi\text{\leavevmode\nobreak\ then\leavevmode\nobreak\ }c(d):\psi$
$\displaystyle(\lambda x:S)c$ $\displaystyle:$ $\displaystyle(\forall
x:S)\,\phi\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\text{if\leavevmode\nobreak\ }\text{forall\leavevmode\nobreak\ }s\in
Dom(S),c[s/x]:\phi[s/x]$ $\displaystyle(s,c)$ $\displaystyle:$
$\displaystyle(\exists x:S)\,\phi\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \text{if\leavevmode\nobreak\ }s\in
Dom(S)\text{\leavevmode\nobreak\ and\leavevmode\nobreak\ }c:\phi[s/x]$

In particular, logical conjunctions of formulas are realized by pairing, and
logical disjunction is realized by elements of disjoint sum, depending on
whether the left- or the right-hand side of the disjunction has been realized.
Logical implication is realized by a function which produces evidence of the
conclusion for each possible assumption. Given the definition
$\phi\,\Rightarrow\,\bot$ for the logical negation of $\phi$, the
realizability rule for logical negation is a special case of the one for
implication. Finally, universal quantification is realized by means of a
function which produces evidence for all possible instantiations, and
existential quantification is realized by a pair consisting of a witness $s$
together with an evidence that this witness indeed satisfies the formula in
the body of the existential quantification.

One way of implementing the BHK explanation of intuitionistic truth for
arithmetic is to associate with each formula $\phi$ some collection of
numerical codes for algorithms which could establish the constructive truth of
$\phi$. Kleene’s realizability semantics of intuitionistic arithmetic, in
particular, assigns such a number $e$ that realizes $\phi$ by induction on the
syntactical structure of the sentence [Kle73]. An arbitrary formula is
realizable if some number realizes its universal closure. In this way, the
number $e$ realizes $\phi\,\land\,\psi$ if $e$ codes a pair $(c,d)$ such that
$c$ realizes $\phi$ and $d$ realizes $\psi$. Likewise, $c$ realizes
$\phi\,\Rightarrow\,\psi$ if, whenever $d$ realizes $\phi$, then the $c$-th
partial recursive function is defined at $d$ and its value realizes $\psi$.
Thus, Kleene’s realizability semantics encodes a proof checker for deciding if
$c$ realizes a given formula $\phi$.

There is a Gentzen-style proof system for Cyberlogic with sequents of the form
$\Gamma\vdash c:\psi$, where $\Gamma$ is a finite set of assumptions of the
form $x_{i}:\phi_{i}$. This proof system admits cut elimination, and
attestation are proven to distribute with logical connectives as follows
[NRRR21].

$\displaystyle{K}\,\rhd\,{\phi\,\land\,\psi}$
$\displaystyle\,\Leftrightarrow\,$
$\displaystyle{K}\,\rhd\,{\phi}\,\land\,{K}\,\rhd\,{\psi}$
$\displaystyle{K}\,\rhd\,{\phi}\,\lor\,{K}\,\rhd\,{\psi}$
$\displaystyle\,\Rightarrow\,$ $\displaystyle{K}\,\rhd\,{(\phi\,\lor\,\psi)}$
$\displaystyle({K}\,\rhd\,{\phi\,\Rightarrow\,\psi})$
$\displaystyle\,\Rightarrow\,$
$\displaystyle({K}\,\rhd\,{\phi})\,\Rightarrow\,({K}\,\rhd\,{\psi})$
$\displaystyle{K}\,\rhd\,{(\nabla x:S)\,\phi)}$
$\displaystyle\,\Leftrightarrow\,$ $\displaystyle(\nabla
x:S)\,{K}\,\rhd\,{\phi}\text{\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ for\leavevmode\nobreak\ }\nabla\in\\{\exists,\forall\\}$

Cyberlogic as investigated in [NRRR21] includes an additional knowledge
modality $\mathrm{KB}_{\mathcal{Q}}({\phi})$, for a set $\mathcal{Q}$ of
principals, with the intended meaning that $\phi$ is derivable from the
collection of local knowledge bases of the principals $\mathcal{Q}$.
Therefore, the operator $\mathrm{KB}_{\mathcal{Q}}({\phi})$ may be read as
“principals in $\mathcal{Q}$ jointly (may) know $\phi$”. In case $\mathcal{Q}$
is the emptyset, we refer to $\phi$ as common knowledge.

The following formula, for example, specifies that for $K$ to attest $\phi$,
both $K_{1}$ and $K_{2}$ need to attest to $\phi$ using only their local
knowledge:

$\mathrm{KB}_{\\{K_{1}\\}}({{K_{1}}\,\rhd\,{\phi}})\,\land\,\mathrm{KB}_{\\{K_{2}\\}}({{K_{2}}\,\rhd\,{\phi}})\,\Rightarrow\,{K}\,\rhd\,{\phi}$

Another use of the knowledge modality is to specify that some evidence should
only be trusted if derived from trusted sources. Consider, for example, three
principals $\mathcal{P}=\\{K_{T},K_{U},K\\}$ where $K$ trusts evidence from
$K_{T}$, but not all evidence from $K_{U}$. Then the following clause

$\mathrm{KB}_{\\{K,K_{T}\\}}({{K}\,\rhd\,{critical(ok)}})\,\land\,\mathrm{KB}_{\mathcal{P}}({{K}\,\rhd\,{nonCritical(ok)}})\,\Rightarrow\,{K}\,\rhd\,{\mathrm{KB}_{\emptyset}({all(ok)})}$

specifies that $K$ can attest that everything is $ok$ as a common knowledge,
i.e. $\mathrm{KB}_{\emptyset}({all(ok)})$, if all the non-critical and
critical elements are $ok$. However, the check of critical parts can only be
performed by principals $K$ trusts, namely $K$ itself or $K_{T}$. In
particular, information from $K_{U}$’s knowledge may not be used in the proof
of $critical(ok)$.

The knowledge modality in Cyberlogic extends the one in linear authorization
logics [GBB+06, Nig14] in that it supports the notion of knowledge shared by
multiple principals. There are a number of interesting properties on knowledge
expressible in Cyberlogic (see [NRRR21]):222 Notice that, strictly speaking,
the logic in [NRRR21] does not include quantification over principals.

$\displaystyle\mathrm{KB}_{\mathcal{Q}}({\phi})$
$\displaystyle\,\Rightarrow\,$ $\displaystyle\phi$
$\displaystyle\mathrm{KB}_{\\{K\\}}({\phi})$ $\displaystyle\,\Rightarrow\,$
$\displaystyle{K}\,\rhd\,{\phi}$
$\displaystyle\mathrm{KB}_{\mathcal{Q}_{1}}({\mathrm{KB}_{\mathcal{Q}_{2}}({\phi})})$
$\displaystyle\,\Rightarrow\,$
$\displaystyle\mathrm{KB}_{\mathcal{Q}_{1}\cup\mathcal{Q}_{2}}({\phi})$

On the other hand, not every fact is known to a set of principals, attestation
of a formula does not imply that the formula is known by the principal, and
the knowledge modality does not commute.

$\displaystyle\phi$ $\displaystyle\not\,\Rightarrow\,$
$\displaystyle\mathrm{KB}_{\mathcal{Q}}({\phi})$
$\displaystyle{K}\,\rhd\,{\phi}$ $\displaystyle\not\,\Rightarrow\,$
$\displaystyle\mathrm{KB}_{\\{K\\}}({\phi})$
$\displaystyle\mathrm{KB}_{\mathcal{Q}_{1}}({\mathrm{KB}_{\mathcal{Q}_{2}}({\phi})})$
$\displaystyle\not\,\Rightarrow\,$
$\displaystyle\mathrm{KB}_{\mathcal{Q}_{2}}({\mathrm{KB}_{\mathcal{Q}_{1}}({\phi})})$

Knowing some attestation is different from attesting to this knowledge (for a
detailed discussion see [NRRR21]).

$\displaystyle\mathrm{KB}_{\mathcal{Q}}({{K}\,\rhd\,{p(t_{1},\ldots,t_{n})}})$
$\displaystyle\not\,\Rightarrow\,$
$\displaystyle{K}\,\rhd\,{\mathrm{KB}_{\mathcal{Q}}({p(t_{1},\ldots,t_{n})})}$

The examples above demonstrate the expressive power of the knowledge modality
in Cyberlogic, and a Cyberlogic interpreter with attestation and knowledge
modalities has been described previously [NRRR21]. In order to keep the
presentation as succinct as possible, however, we will not explicitly mention
the case of Cyberlogic policies with knowledge modalities in the remainder of
this exposition.

##  Chapter 3 Distributed Proof Search

Given a logical context $\Gamma$ of the form
$x_{0}:\phi_{0},\ldots,x_{n}:\phi_{n}$, for some $n\in Nat$, and a formula
$\psi$, the problem of proof search is to determine a proof $c$ such that
$\Gamma\,\vdash\,c:\psi$. Clearly, proof search for first-order intuitionistic
logic, and therefore also for Cyberlogic, is undecidable. The problem of
checking if some given proof actually proves some statemeent, on the other
hand, usually is of low polynomial complexity.

For distributed proof search, we assume a certain number of principals $K$ in
Cyberlogic. We also assume that each of these principals has a local logical
context $\Gamma(K)$. These local contexts form the policies of the principals
$K$, as they form the basis for $K$’s own (local) deductive proof search
capability. In this way, proof search may proceed locally until there is a
subgoal which needs to be handed-off to another principal. We refer to this
integrated process of local deduction and the communication of subgoals and
(partial) solutions between authorities as distributed proof search.

Policy $\Gamma(A)$

$\displaystyle a_{1}$ $\displaystyle:$
$\displaystyle{A}\,\rhd\,{isHospital(C)}$ $\displaystyle a_{2}$
$\displaystyle:$ $\displaystyle(\forall
X:Physician,Y:Patient)\,isPhysicianOf(X,Y)$ $\displaystyle\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\,\Rightarrow\,{A}\,\rhd\,{readMedRec(X,Y)}$ $\displaystyle a_{3}$
$\displaystyle:$ $\displaystyle(\forall X:Physician,Y:Patient,Z:Hospital)$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
{A}\,\rhd\,{isHospital(Z)}\,\land\,({Z}\,\rhd\,{isPhysicianOf(X,Y)})$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\,\Rightarrow\,{A}\,\rhd\,{isPhysicianOf(X,Y)}$ $\displaystyle a_{4}$
$\displaystyle:$ $\displaystyle(\forall H,Z_{1},Z_{2}:Hospital)\,Z_{1}\neq
Z_{2}\,\land\,Z_{1}\neq A\,\land\,Z_{2}\neq A$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\,\land\,{A}\,\rhd\,{isHospital(Z_{1})\,\land\,isHospital(Z_{2})}$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\,\land\,({Z_{1}}\,\rhd\,{isHospital(H)}\,\lor\,{Z_{2}}\,\rhd\,{isHospital(H)})$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\,\Rightarrow\,{A}\,\rhd\,{isHospital(H)}$

Policy $\Gamma(B)$

$\displaystyle b_{1}$ $\displaystyle:$
$\displaystyle{B}\,\rhd\,{isHospital(A)}$ $\displaystyle b_{2}$
$\displaystyle:$ $\displaystyle{B}\,\rhd\,{isHospital(B)}$ $\displaystyle
b_{3}$ $\displaystyle:$ $\displaystyle{B}\,\rhd\,{isPhysicianOf(Alice,Peter)}$

Policy $\Gamma(C)$

$\displaystyle c_{1}$ $\displaystyle:$
$\displaystyle{C}\,\rhd\,{isHospital(B)}$

Figure 3.1: Scenario of hospital policies for accessing medical records.

We illustrate distributed proof search by means of a simple example for
accessing medical records. There are three hospitals with names $A$, $B$, $C$
with corresponding authorities. The access policies $\Gamma(A)$, $\Gamma(B)$,
and $\Gamma(C)$ for the three hospitals are depicted in Figure 3.1. For
instance, $a$ attests to the facts that $b$ and $c$ are hospitals, and $a_{2}$
encodes the rule that every physician of some patient can read her medical
records. Assumption $a_{3}$ allows $A$ to delegate the decision on the
physician-patient relationship to some hospital $Z$; more precisely, if
hospital $Z$ attests to a certain physician-patient relationship then $A$
attests to the truth of this relationship.

Now, assume that some evidence needs to be constructed that indeed physician
$Alice$ can access the medical records of patient $Peter$.

$\displaystyle?_{0}$ $\displaystyle:$
$\displaystyle{A}\,\rhd\,{readMedRec(Alice,Peter)}$

Here, $?_{0}$ is a (meta-)variable for the evidence which needs to be
constructed. We use the assumptions of the individual policies in Figure 3.1
to iteratively collect constraints on these meta-variables. In a first step,
we apply hypothesis $a_{2}$ to $Alice$ and $Peter$ to obtain the new subquery.

$\displaystyle?_{1}$ $\displaystyle:$
$\displaystyle{A}\,\rhd\,{isPhysician(Alice,Peter)}$

Since $?_{0}\equiv a_{2}(Alice)(Peter)(?_{1})$ one can construct an evidence
of the top query from a solution for $?_{1}$. In proof search these kinds of
reductions are called backward chaining, and their application relies on
matching (possibly modulo theories) the current query with the conclusion of a
universally quantified implication. In this way, the correspondingly
instantiated premises of this implication serve as the new subqueries. In a
next step, we backchain on assumption $a_{3}$ to obtain

$\displaystyle?_{2}$ $\displaystyle:$
$\displaystyle{A}\,\rhd\,{isHospital(Z)}$ $\displaystyle?_{3}$
$\displaystyle:$ $\displaystyle{Z}\,\rhd\,{isPhysicianOf(Alice,Peter)}$

with $?_{1}\equiv a_{3}(Alice)(Peter)(Z)(?_{2})(?_{3})$. Thus, one needs to
find a hospital $Z$ which attests to this physicial-patient relationship. This
is a fact in the policy of hospital $B$, and consequently $?_{3}\equiv B$ and
$Z\equiv B$. Thus, we are reduced to show that $A$ can attest that $B$ indeed
is a hospital. Backchaining on rule $a_{4}$ we need to find two hospitals
distinct of $A$ which are attesting that $B$ indeed is a hospital.

$\displaystyle?_{5}$ $\displaystyle:$ $\displaystyle Z_{1}\neq
Z_{2}\,\land\,Z_{1}\neq A\,\land\,Z_{2}\neq A$ $\displaystyle?_{6}$
$\displaystyle:$
$\displaystyle{A}\,\rhd\,{isHospital(Z_{1})}\,\lor\,{A}\,\rhd\,{isHospital(Z_{2})}$
$\displaystyle?_{7}$ $\displaystyle:$
$\displaystyle{Z_{1}}\,\rhd\,{isHospital(B)}\,\land\,{Z_{2}}\,\rhd\,{isHospital(B)}$

Here, $?_{2}\equiv a_{4}(B)(Z_{1})(Z_{2})(?_{5})(?_{6})(?_{7})$. With
$Z_{1}\equiv B$ and $Z_{2}\equiv C$ we obtain $?_{6}\equiv inr(a_{1})$,
$(?_{7}\equiv(b_{2},c_{1})$, and $?_{5}$ is obtained from the corresponding
background theory ("all hospitals are not equal"). This concludes the
construction, and evidence $?_{0}$ for the original query is obtained by back-
substitution:

$\displaystyle a_{2}(Alice)(Peter)$ $\displaystyle\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ (a_{3}(Alice)(Peter)(B)$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
(a_{4}(B)(B)(C)$ $\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ (\\_)(inr(a_{1})(b_{2},c_{1}))$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ (b_{3}))$

We left a "hole" $(\\_)$ for the proof term for the query $?_{5}$ as obtained
from the background theory. Decision procedures for certain background
theories may be used to fill in these kinds of "holes" when needed. This may
result in drastically reduced sizes of proof terms, but at the expense of
increased effort for checking evidence.

Policy $\Gamma(CA)$

$\displaystyle ca_{1}$ $\displaystyle:$ $\displaystyle(\forall
x:Object)\,\mathrm{DL}[{CA}\,\to\,{HMO}]\,{isHospital(x)}$

Policy $\Gamma(HMO)$

$\displaystyle hmo_{1}$ $\displaystyle:$ $\displaystyle(\forall
K:Principal,\,x:Object)\,(K=A\lor(K=B\lor K=C))\,\Rightarrow\,$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
{K}\,\rhd\,{isHospital(x)}\,\Rightarrow\,{HMO}\,\rhd\,{isHospital(x)}$

Figure 3.2: Example for hospital policies and delegation.

Incremental synthesis of proof terms in intuitionistic logic by means of back-
chaining is supported by proof development systems such as Coq [PM11]. In our
case, however, the proof search is distributed between several collaborating
authorities. Consider, for example, the situation above where $A$ needs to
find a hospital $Z_{1}(\neq A)$ with ${Z_{1}}\,\rhd\,{isHospital(B)}$.
Clearly, given its policy $\Gamma(A)$, the authority $A$ can not progress on
solving this subquery, and consequently initiates a broadcast to applicable
authorities. In the example, above both $B$ and $C$ respond successfully, and
$A$ is able to attest that both respondents are indeed hospitals.
Alternatively, $a$ may selectively only query authorities for which it is able
to attest that they indeed are hospitals. Similar strategies for distributed
proof search, in particular, the interaction between local and global proof
search, have recently been studied, for example, in [NRRR21, NRB+20].

The proof term as generated above may be used as evidence that $Alice$ has
access to the medical records of $Peter$. Indeed, a gatekeeper, physical or
not, of the requested medical records may verify access rights by checking
that the presented proof term supports the requested access. These kinds of
proof checks can be performed in low polynomial time in the size of the proof
term.

There are however a number of disadvantages to this style of proof-carrying
authorization in real-world applications. First, proof checking requires
access to all policies. Despite all the wishes for transparency on policies,
this does not seem to be a realistic proposition. For example, it seems highly
unlikely that all authorities involved in a visa application process make all
of their decision policies widely accessible. Second, proof terms represent
tree-like derivations which may be growing arbitrarily large. There are some
techniques of shrinking proof trees. For example, proof terms for decidable
fragments (for example, background theories such as Presburger arithmetic) may
be omitted, since these proofs can always be reconstructed. Other proof-
theoretic techniques for compact representations of proofs such as midsequents
[Gal15] and focusing [NRRR21]) are also based on trading space for
representing proofs with the time for proof checking [Mil15]. We will address
these issues in some more detail in 6.

##  Chapter 4 Expressiveness

###  4.1 Authorization and Delegation

The attestation ${K}\,\rhd\,{\phi}$ does not logically imply the validity of
$\phi$. Such a validity only follows when principal $K$ possesses authority
over $\phi$; namely:

<EMAIL_ADDRESS>
Consider, for example, a principal $\mathrm{A}$ for deciding the theory of
linear arithmetic. Trust on principal $\mathrm{A}$ to be correct in the sense
that it only attests valid arithmetic formulas may be expressed through the
authority ${A}\,\rhd\,{\phi}\,\Rightarrow\,\phi$ for all $\phi$ in the
language of linear arithmetic.

Such an authority of a key must itself be attested by a certification
authority. Let’s assume a single ’top-level’ certification authority $CA$ with
the assumption that anything attested by this certification authority is
valid. Thus, for all $\phi$: $({CA}\,\rhd\,{\phi})\,\Rightarrow\,\phi$. A
principal $K$ can selectively authorize another principal $L$ through

<EMAIL_ADDRESS>
This kind of delegation of the authority over certain formulas
$p(x_{1},\ldots,x_{n})$ from a principal $K$ to a principal $L$ may also be
denoted by $\mathrm{DL}[{K}\,\to\,{L}]\,{\phi}$. In this way, the
certification authority $CA$ in Figure 3.2 delegates the authority on
$isHospital$ to a principal $HMO$, which itself chooses to attest to
$isHospital$ only if one of its hospital principals $A$, $B$, or $C$ does so.

Likewise, the authority of $visa(\\_)$ in our running example on issuing visa
certificates may be selectively delegated to certain consulates by the State
Department. Such a delegation might also be realized through a chain of
delegation. And, indeed, indirect delegation is definable in Cyberlogic as
follows:

${K}\,\rhd\,{(\forall
<EMAIL_ADDRESS>
Moreover, indirect delegation can be iterated to an arbitrary finite depth.
Initial versions of Cyberlogic distinguished between direct and indirect
attestations, where direct attestations were used to restrict the capability
of further delegation. However, the proof theory of Cyberlogic with direct and
indirect attestations does not admit cut-elimination [Rei19], and has
therefore been omitted.

###  4.2 Timed Attestation

Time is often needed to establish that a piece of evidence was produced before
or after a certain point in time. The $Time$ domain for representing instances
of time is infinite, it admits an equality relation $=$, and it is totally
ordered by $<$; otherwise, the $Time$ domain is uninterpreted. For the
certification of time we assume a trusted time source $T$ of sort $Principal$
and a unary predicate $time(t)$ for attesting that a specific time instant $t$
has passed; that is:

$\displaystyle c$ $\displaystyle:$
$\displaystyle{T}\,\rhd\,{time(t)}\mbox{\@,}$

where $c$ certifies that time $t$ has elapsed if $Decr(Pub(T),\,c)$ yields
$time(t)$.

The following definitions are used for specifying whether some point in time
$t$ has elapsed or not, or if it is current.

$\displaystyle past(t)$ $\displaystyle:=$ $\displaystyle(\exists
s:Time)\,s>t\,\land\,\ {T}\,\rhd\,{time(s)}$ $\displaystyle future(t)$
$\displaystyle:=$ $\displaystyle(\forall s:Time)\,s\geq
t\,\Rightarrow\,\lnot\,({T}\,\rhd\,{time(s)})$ $\displaystyle curr(t)$
$\displaystyle:=$ $\displaystyle{T}\,\rhd\,{time(t)}\land(\forall
s:Time)\,{T}\,\rhd\,{time(s)}\,\Rightarrow\,s\leq t$

Time-stamped certificates are embedded in other certificates to establish that
a piece of evidence was produced following time $t$.

$\displaystyle{K}\,\rhd_{{\small{\mathrm{aft}({t})}}}\,{\phi}$
$\displaystyle:=$
$\displaystyle{K}\,\rhd\,{\phi}\,\land\,{T}\,\rhd\,{time(t)}$

Therefore, $c$ realizes this timed attestation if $Decr(Pub(K),\,c)$ yields a
representation of a pair $(c,d)$ such that $c$ certifies ${K}\,\rhd\,{\phi}$
and $d$ certifies ${T}\,\rhd\,{time(t)}$. The situation here is similar to
hijackings scenes in the movies, where the culprit sends a picture of a
hostage together with a recent issue of a newspaper to provide evidence of her
relative well-being at a point of time after the newspaper has been issued.

To demonstrate that a claim ${K}\,\rhd\,{\phi}$ was produced prior to time
$t$, we once again rely on the trusted time source $T$ to timestamp the claim.
The attestation ${T}\,\rhd_{{\small{\mathrm{bef}({t})}}}\,{\phi}$ indicates
that the trusted time source $T$ attests to $\phi$ being verifiable prior to
time $t$. In this case, the certificate $c$ is evidence for
${T}\,\rhd_{{\small{\mathrm{bef}({t})}}}\,{\phi}$ if $Decr(Pub(T),\,c)$ yields
$(\phi,t)$. Since $T$ is a trusted time source, its timed attestations can be
taken as valid, so that
${T}\,\rhd_{{\small{\mathrm{bef}({t})}}}\,{{K}\,\rhd\,{\phi}}\,\Rightarrow\,{K}\,\rhd_{{\small{\mathrm{bef}({t})}}}\,{\phi}$.

Finally, temporal modalities are definable in Cyberlogic using timed
attestations ($t$ is of sort $Time$).

$\displaystyle\Diamond({K}\,\triangleright\,{\phi})(t)$ $\displaystyle:=$
$\displaystyle{K}\,\rhd_{{\small{\mathrm{aft}({t})}}}\,{\phi}$

Thus, $\Diamond({K}\,\triangleright\,{\phi})$ holds at time $t$ if $K$ attests
to $\phi$ at some latter point of time. These kinds of encodings are used for
defining a temporal logic by pointwise lifting the logical connectives to the
time domain, and for deriving corresponding inference rules in the usual way.
Past-time temporal operators are encoded in a similar manner. Moreover,
interval-based temporal operators such as
$\Box_{[{t_{1}},{t_{2}}]}({K}\,\triangleright\,{\phi})$, which expresses that
$k$ always attests to $\phi$ in the time interval $[t_{1},t_{2}]$ and, more
generally, Allen-style [AH89] operators such as $\mathrm{Before}$,
$\mathrm{After}$, $\mathrm{During}$, and $\mathrm{Overlaps}$ are also
definable.

###  4.3 Revocation of Authority

Timestamping can be used to ensure that revocable certificates have not been
revoked at a given time. This can be done by ensuring that the authority
granted by the certification authority $CA$ is fresh, as given by

<EMAIL_ADDRESS>
However, this mechanism does not specify that the authority is revocable. A
revocable delegation of authority from $K$ to $L$ can be specified as

<EMAIL_ADDRESS>
This formula asserts that if $K$ attests that $L$’s authority has not been
revoked up to time $t$, then any attestation by $L$ of the statement $\phi(s)$
for $s<t$ is tantamount to an attestation by $K$ of $\phi(s)$.

This simple mechanism demonstrates how revocation of authorities can be
encoded in core Cyberlogic. Clearly, more refined revocation mechanisms are
possible, for example by restricting the authority over certain formulas or to
allow for undoing revocations.

###  4.4 Nonces

Another mechanism for ensuring the freshness of evidence is through the use of
nonces, which can be thought of as unique numbers which are hard or impossible
to guess. We therefore assume a trusted principal $N$ for generating nonces
$n$ by means of asserting:

<EMAIL_ADDRESS>
Uniqueness of the nonces is expressed by the assumption

$(\forall n,m:Nonce,s,t:Time)\,s\neq
t\land{N}\,\rhd_{{\small{\mathrm{at}({s})}}}\,{nonce(n)}\land{N}\,\rhd_{{\small{\mathrm{at}({t})}}}\,{nonce(m)}\,\Rightarrow\,n\neq
<EMAIL_ADDRESS>
where ${N}\,\rhd_{{\small{\mathrm{at}({t})}}}\,{nonce(.)}$ denotes attestation
of $nonce(.)$ at time point $t$.

A common mechanism in protocols is that one participant in a protocol
challenges another participant to produce evidence with a newly generated
number, the nonce, so as to ensure recency of the evidence. These kinds of
mechanisms have previously been formalized in terms of logic in the context of
specifying security protocols [DLMS04]. In this way, we will also be using
logical instantiation rules for generating nonces while executing security
protocols (see Section 5).

###  4.5 Distibuted Logic Programs

Transactions and protocols are implemented as distributed logic programs. The
policies in Figure 3.1, for example, can easily be expressed as universally
closed Horn formulas of the form
$\phi_{1}\,\land\,\ldots\,\land\,\phi_{n}\,\,\Rightarrow\,\,\phi$, where each
$\phi_{i}$ and $\phi$ is either an atom or an atomic attestation of the form
${k}\,\rhd\,{\psi}$, where $\psi$ is an atom. A corresponding query is an atom
or atomic attestation such as ${a}\,\rhd\,{readMedRec(Alice,Peter)}$ (see
Section 3), and the logical derivation of this query from the union of
individual policies is based on an operational reading of Horn clauses, called
backchaining, for successively reducing queries $\phi$ to subqueries
$\phi_{1},\ldots,\phi_{n}$.

The example in Section 3) also demonstrates the three basic steps of the
distributed execution of Cyberlogic programs for proof search of queries, as,
in each execution step, either (1) a query is decomposed into subqueries, or
(2) a query is sent from a supplicant to an appropriate authority, or (3)
there is a reply to a query in the form of a (partial) proof sent back to the
supplicant. The steps (2) and (3) for communicating queries and partial
solutions between principals may also be decoupled further using a distributed
coordination mechanism such as Linda [GC92]. These kinds of blackboard
architectures also support queries such as $(\exists
X:Principal)\,{X}\,\rhd\,{p(42)}$ when an adequate addressee for solving this
query has not been determined by the principal issuing this query. These
generalized queries are reminiscent of multicast broadcasting.

Cyberlogic programs are based on a slight extension of Horn formulas, which
are called (first-order) hereditary Harrop formulas. These formulas extend the
logic of Horn clauses by permitting implication and universal quantification
in queries, and they consist of D-formulas (programs) and G-formulas (queries)
[MNPS91].

$\displaystyle D$ $\displaystyle::=$ $\displaystyle
Atom\;|\;G\,\Rightarrow\,Atom\;|\;(\forall x)D\;|\;D\,\land\,D$ $\displaystyle
G$ $\displaystyle::=$ $\displaystyle
Atom\;|\;G\,\land\,G\;|\;G\,\lor\,G\;|\;(\exists
x)\,G\;|\;D\,\Rightarrow\,G\;|\;(\forall x)G$

Here, Atom is any atom or an atomic attestation modality. These formulas
define a logic programming language in that a G-formula can be thought of as a
query (or goal), a finite set of D-sentences constitutes a program, and the
process of answering a query consists of constructing an intuitionistic proof
of the existential closure of the query from the given program. In this way,
hereditary Harrop formulas constitute an abstract logic programming language
[MNPS91], since the declarative reading of the logical connectives coincides
with the search-related reading. A query of the form $D\,\Rightarrow\,G$, in
particular, can be interpreted as an instruction to augment the program with
$D$ in the course of solving $G$, and a query of the form $(\forall x)\,G$ can
be interpreted as an instruction to generate a new name and to use it for $x$
in the course of solving $G$.

This operational reading of Cyberlogic formulas yields a proof procedure for
the logic of hereditary Harrop formulas [Nad93]. This proof procedure is based
on searching for uniform proofs [MNPS91] in the logic of hereditary Harrop
formulas, and uses concepts such as dynamic Skolemization [Fit12] and
unification of terms embedded under arbitrary sequences of quantifiers for
controlling the search for instantiations of existentially quantified goal
formulas. This proof procedure can be extended to higher-order hereditary
Harrop formulas, which are used in the higher-order logic programming language
$\lambda$Prolog. Indeed, early Cyberlogic interpreters have been realized as
deep embeddings in $\lambda$Prolog [Ber06].

A large number of protocols and policies may already be encoded as variants of
Horn-clause logic programs. In this way, we have identified a Horn-clause like
fragment of Cyberlogic, and proposed a (focused) proof systems for sound and
complete proof search [NRRR21].

Datalog is even less expressive as it restricts Horn-clause logic programs to
atoms of the form $p(a_{1},\ldots,a_{n})$, where each $a_{i}$ either is a
variable or a constant symbol. Indeed, Datalog is attractive in that it
supports the evaluation of recursive programs, it may be extended with built-
in predicates (which evaluate variable-free atoms) [LM03], supports
(stratified or well-founded) negation [ZS95], and may be executed in a
distributed manner [ABGR10]. Datalog with stratified negation, in particular,
has been instrumental in expressing a number of non-trivial policies [LMS09].
ETB Datalog, in addition, has well-defined denotational111ETB Datalog uses an
unbounded Herbrand universe in contrast to vanilla Datalog and distributed
operational semantics [CHM+14], it generalizes built-in predicates to
interpreted predicates, and ETB Datalog may generates certificates. Finally,
the Cyberlogic interpreter in [NRRR21] is unique in that it supports (focused)
execution of programs with both attestation and knowledge modalities.

##  Chapter 5 Cryptographic Protocols

We are using the infamous Needham-Schroeder [Low96] authentication protocol
for demonstrating the expressive power of Cyberlogic and distributed proof
search for formalizing and executing cryptographic protocols. The textbook
presentation of the Needham-Schroeder protocol specifies the sequence of
messages between senders and intended recipients.

$\displaystyle A\to B$ $\displaystyle:$ $\displaystyle\\{A,N_{a}\\}_{Pub(B)}$
$\displaystyle B\to A$ $\displaystyle:$
$\displaystyle\\{B,N_{a},N_{b}\\}_{Pub(A)}$ $\displaystyle A\to B$
$\displaystyle:$ $\displaystyle\\{N_{b}\\}_{Pub(B)}$

In a first step, principal $A$ sends $B$ an encrypted message containing both
the name of the sender together with a nonce $N_{a}$, which has been generated
by $A$ for this purpose. Principal $B$ responds by generating a nonce $N_{b}$,
conjoining it with the nonce $N_{a}$ as obtained by $A$ together with its name
$B$, and sending the encrypted message to $A$. In a third step, $A$
acknowledges receipt of this message to $B$. The goal of this protocol is to
generate a secret number, which is known to the principals $a$ and $b$, but
nobody else. From this informal description it should become evident that the
textbook description above on the Needham-Schroeder sequence of message
exchanges does not make the details for executing the protocol explicit. A
complete formalization in logic of these kinds of security protocols has been
developed, for example, in [MR00].

It turns out that the hereditary Harrop formulas of Cyberlogic are expressive
enough to succinctly formalize cryptographic protocols such as Needham-
Schroeder authentication. In fact, principal $A$ initiates a Needham-Schroeder
protocol round by querying principal $B$ based on the Cyberlogic formula
below, and $B$ responds using the same Cyberlogic program $NSP(A,B)$, which is
defined as

$\displaystyle(\forall x_{a}:Nonce)$ $\displaystyle\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ ((\forall
x_{b}:Nonce)\,{B}\,\rhd\,{msg_{3}(x_{b})}\,\,\Rightarrow\,\,{A}\,\rhd\,{msg_{2}(B,x_{a},x_{b})})$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
<EMAIL_ADDRESS>
Thus, $NSP(A,B)$ represents one round of the Needham-Schroeder protocol
between principals $A$ and $B$. In initiatiating such a round, $A$ first
chooses a (constant) nonce $N_{a}$111To keep this exposition as simple as
possible $A$ just chooses an arbitrary integer without any considerations on
the freshness of this choice. and queries $B$ to provide evidence $?_{0}$ that
it attests to $msg_{1}(A,N_{a})$.

$\displaystyle h_{a}$ $\displaystyle:$ $\displaystyle((\forall
x_{b}:Nonce)\,{B}\,\rhd\,{msg_{3}(x_{b})}\,\,\Rightarrow\,\,{A}\,\rhd\,{msg_{2}(B,N_{a},x_{b})})$
$\displaystyle?_{0}$ $\displaystyle:$
$\displaystyle{B}\,\rhd\,{msg_{1}(A,N_{a})}$

Now, $B$ backchains based on its program and selects, as above, a nonce
$N_{b}$ to obtain the subquery in its extended local context.

$\displaystyle h_{b}$ $\displaystyle:$
$\displaystyle{B}\,\rhd\,{msg_{3}(N_{b})}$ $\displaystyle?_{1}$
$\displaystyle{A}\,\rhd\,{msg_{2}(B,N_{a},N_{b})}$

Principal $B$ now queries $A$ to provide such an evidence $?_{1}$ for its
attestation to $msg_{2}(B,N_{a},N_{b})$. Principal $A$ responds to this query
by backchaining on program $h_{a}$ after instantiating it with the nonce
$N_{b}$ as obtained through the message $msg_{2}$ from $B$. This results in
the subquery

$\displaystyle h_{a}$ $\displaystyle:$ $\displaystyle((\forall
x_{b}:Nonce)\,{B}\,\rhd\,{msg_{3}(x_{b})}\,\,\Rightarrow\,\,{A}\,\rhd\,{msg_{2}(B,N_{a},x_{b})})$
$\displaystyle?_{2}$ $\displaystyle:$
$\displaystyle{B}\,\rhd\,{msg_{3}(N_{b})}$

which is communicated and delegated to $B$. This query is solved trivially by
hypothesis $h_{b}$.

This concludes the distributed execution for solving $A$’s query. Notice that
the subqueries as communicated back-and-forth between the principals $A$ and
$B$ in the derivation above are exactly the plain text versions of the
messages of one round of the Needham-Schroeder protocol, and they occur in
exactly the same order. If communication channels between principals is
insecure, we may, following the Needham-Schroeder protocol above, only
communicate queries encrypted by the public key of the intended recipient.

The construction of the proof term for the original query from its subqueries
is immediate from the realizability semantics of Cyberlogic. Such a proof term
is useful for verifying that the result has been obtained in a manner
compliant with the Needham-Schroeder protocol. It does not, however, directly
entail the crucial secrecy property of the Needham-Schroeder protocol itself.
Cyberlogic’s knowledge modality may be used for expressing secrecy properties
of the Needham-Schroeder protocol.

$\displaystyle NSP(A,B)$ $\displaystyle\,\Rightarrow\,$ $\displaystyle(\exists
N:Nonce)\,\,\mathrm{KB}_{\\{A\\}}({nonce(N)})\,\land\,\mathrm{KB}_{\\{B\\}}({nonce(N)})$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\,\land\,(\forall K:Principal)\,(K\neq A\,\land\,K\neq B)$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\
\,\Rightarrow\,\lnot\,{\mathrm{KB}_{\\{K\\}}({nonce(N)})}$

That is, after one round of the Needham-Schroeder protocol between principals
$A$ and $B$, these principals share a secret which nobody else knows. These
kinds of secrecy properties for cryptographic protocols are established by
means of inductive secrecy invariants [MR00].

The above derivation demonstrates that the operational semantics of the
respective contexts of the principals determines the construction of the next
subquery / message at any specific point of time. The semantics of the logical
connectives therefore provide all the necessary details and the right kind of
scoping of variables for continuing executing the Needham-Schroeder protocol.
In fact, these local contexts can be thought of as continuations. For
sequential protocols such as Needham-Schroeder there is no don’t know non-
determinism in the operational proof search as the choice of the nonces is
arbitrary. And, therefore, distributed proof search might simply be realized
by interacting coroutines for each principal which are switching control
according to continuations based on local proof search.

##  Chapter 6 Privacy of Policies

Evidence checking as outlined above requires a complete proof tree and also
access to all policies. These are strong assumptions, indeed, as tree-like
proof terms may grow arbitrary large, and not all principals are ready to be
completely transparent with respect to their policies. The size of the proof
trees may simply be reduced by node sharing, for example, by maintaining the
hashs of proof nodes in a tamper-proof lookup table. For supporting evidential
transactions betweeen principals with private policies, we propose the use of
functional encryption schemes [BSW11].

A proof/evidence checker for Cyberlogic is a function $check_{\Gamma}(e,\phi)$
which returns $ok$ if $\Gamma\vdash e:\phi$, and $nok$ otherwise. A proof
checker for the principal $HMO$ with the logical context $\Gamma(HMO)$ in
Figure 3.2, for example, is derived directly from the structure of the single
policy rule $hmo_{1}$.

$\displaystyle\mathrm{check}_{\Gamma(HMO)}(e,\phi)\leavevmode\nobreak\ =$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\mathbf{cases}\leavevmode\nobreak\ \phi\leavevmode\nobreak\ \mathbf{of}$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
({HMO}\,\rhd\,{isHospital(x)})\leavevmode\nobreak\ :$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\mathbf{cases}\leavevmode\nobreak\ Decr(Pub(HMO),e,\,\leavevmode\nobreak\
)\mathbf{of}$ $\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ hmo_{1}(A)(x)(inl(\\_))(d)\leavevmode\nobreak\
:\leavevmode\nobreak\
\mathrm{check}_{\Gamma(A)}(d,{A}\,\rhd\,{isHospital(x)})$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\ \ldots$
$\displaystyle\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\mathbf{otherwise}\leavevmode\nobreak\ :\leavevmode\nobreak\ nok$

If evidence for attestations are hashed, then proof terms are obtained from a
lookup table, thereby avoiding the need to communicate large proof trees.

The definition of the proof checker above requires knowledge about all local
policies involved in building up the evidence. Therefore, if principals decide
to keep respective policies secret then verifiable proof-carrying
authorization as outlined above does not work anymore. We demonstrate a
possible way forward to keep such a checker secret and still be able to apply
it for verifying specific authorities. This approach is inspired by functional
encryption [BSW11], which, given a function $f$ constructs a key pair
$(Pub(f),Prv(f))$ such that $f(x)$ can be computed as
$Decr(Prv(f),\,Encr(Pub(f),\,x))$. In this way, the function $f$ may be
evaluated by a third party (say, the "cloud") without revealing arguments $x$
to this untrusted party.

The situation here is slightly different as we are interested in keeping the
function, namely the proof checker secret, whereas the argument $(c,\varphi)$,
which includes a certificate $c$, may be public knowledge. Therefore, given a
checker $check_{\Gamma}$, which is only known to the principal with policy
$\Gamma$, we assume the existence of key pairs
$(Pub(check_{\Gamma}),Prv(check_{\Gamma}))$ such that

<EMAIL_ADDRESS>
In this way, a certificate $c$ is verified by means of (a partial evaluation)
of composing encryption followed by decryption using the functional encryption
pair for $check_{\Gamma}$, and without revealing the policy $\Gamma$. As such,
our traveler presents a certificate to the border control which checks, using
the functional key pair for the proof checker of the consulate $Cons42$ for
permission of entry.

The functional encryption scheme is also used for the incremental maintenance
of policies and certificates. This requires adding a hash value $Hash(\Gamma)$
to certificates and the maintenance of a tamper-proof log of the publicly
accessible table $Hash(\Gamma)\mapsto check_{\Gamma}$, which is used for
looking up the appropriate proof checker for the policy $\Gamma$. Whenever a
principal updates its policy, a new entry to this lookup table is generated.
These changes may also require to recursively update all dependent policies.
Certificates which have been generated with outdated policies, can still be
checked as the corresponding functional key pair is being kept as part of the
lookup table.

It is at least unusual to publish both the public and the secret key, and
there is a chance that the checker and the actors’ policies, which are
supposed to be kept private, might be reconstructed from this key pair. It
should therefore be interesting to investigate the possibility of generating a
single key for replacing proof checking with decryption. Clearly, the checker
might also be approximated inductively from observing its outputs, which needs
to be restricted.

A possible way forward for ensuring that $\Gamma$ remains private is based on
multi-input functional encryption [GKL+13, GGG+14], which generalizes
functional encryption to $n$-ary functions both in public-key and the
symmetric-key settings. Here, a user in possession of a token $TK_{f}$ for an
$n$-ary function $f$ and multiple ciphertexts $Encr(.,\,x_{1})$, …,
$Encr(.,\,x_{n})$ can compute $f(x_{1},...,x_{n})$ but nothing else about the
arguments $x_{i}$. We therefore consider the proof checker $check$ as the
uncurried binary function $check(\Gamma,(c,\phi))$. Now, a multi-input
functional encryption scheme can be used for encrypting the two arguments
$\Gamma$ and $(c,\phi)$ separately. The function $check$ can then be applied
to these arguments without revealing anything about the arguments. The point
is that the encryption scheme ensures that the information in $\Gamma$ remains
private. The function $check$ therefore may be published without revealing the
policy $\Gamma$.

The original design of Cyberlogic [RS03] has been influenced heavily by the
trust management view of authorization in open, large-scale, distributed
systems [BFL96, EFL+99, LGF03, CFL+97]. This view adopts a key-centric
perspective of authorization, since public keys are treated as principals and
direct authorization. There is also a long tradition of encoding authorization
policies in terms of logic programs (for example, [LM03, And03]), and proof-
carrying authorization has also been proposed previously [AF99].

The novelty of Cyberlogic is largely due to the combination of its three key
ingredients: first, the identification of public keys with authorities,
second, the specification of authorization policies as distributed logic
programs, and third, the construction of verifiable and tamper-proof evidence
by distributed proof search. This combination makes Cyberlogic expressive
enough for encoding a number of all-important policy mechanisms such as
revocation and delegation [LGF03], which previously have been custom-built
into specialized trust management systems or added in a rather ad hoc manner.

Cyberlogic has found a number of different applications over the years. For
instance, Cyberlogic has been proposed for producing nonrepudiable digital
evidence sound enough to withstand court challenges [GKS09], as an enabling
mechanism for accountable clouds [GCS13], for generating safety cases [BC21],
for specifying smart legal contracts [DKTPG18, DPTP18] \- since trusting the
majority of system nodes in a blockchain does not need to be assumed any more
with verifiable and possibly proof-carrying computation, for enabling
accountability in federated machine learning [BAP+22, BSK+21] including
verifiability, undeniable consent, auditability, and tamper-evidence, and,
recently, also for assuring the trustworthiness of increasingly autonomous
systems [Rue22].

DKAL is a declarative authorization language for distributed systems [GN08],
which shares the Cyberlogic vision of logic and proof-based authorization in
distributed systems. The basic setup of Cyberlogic and DKAL are similar, in
that DKAL also is a language for writing the policies of a distributed
system’s interacting principals, each DKAL principal performs its own
computations and deductions, and the system has no central logic engine but
merely provides an infrastructure supporting reliable communication between
principals [BDCG12]. Also, each principal works with a knowledge base that can
be modified as a result of communications from other principals or as a result
of deduction. Principals in DKAL, however are communicating by sending each
other items of information, called infons, whereas Cyberlogic principals
communicate queries and answers to these queries in the process of distributed
proof search. Also, the main aim of DKAL is to exceed the expressivity of the
Datalog-based SecPal [BFG10] trust management system in a number of useful
ways and yet to maintain feasible complexity bounds for answering
authorization queries [GN08].

DKAL may be viewed as a conservative extension of disjunction-free
intuitionistic logic [GN09], where trust is definable. For example statements
such as ’k is trusted on saying x’, for an infon $x$, logically means
$(k\,said\,x)\,\Rightarrow\,x$ in DKAL. This is reminiscent of the encoding of
authority $({K}\,\rhd\,{\phi})\,\Rightarrow\,\phi$ of principal $K$ over
certain properties $\phi$ in Cyberlogic. Both Cyberlogic and DKAL are based on
different extensions of intuitionistic logics with an attestion modality. But
DKAL chooses a disjunction-free propositional intuitionistic logic for its
emphasis on efficient query answering, whereas Cyberlogic is based on a more
expressive first-order intuitionistic logic. Thus Cyberlogic is more general
than DKAL, at the expense of decidability and low complexity query answering.
Moreover, and in contrast to Cyberlogic, query answering in DKAL is not based
on executing distributed logic programs and it does not support evidential
authorization, even though there has been an initial proposal for an
evidential DKAL, where communicated information is accompanied with sufficient
justification [BGMN11]. Finally both distributed authorization logics
distinguish between knowing and attesting, but the knowledge modality in
Cyberlogic also supports knowledge shared by multiple principals. Therefore it
should be possible to embed DKAL-like authorization systems into Cyberlogic,
and to benefit from DKAL’s efficient query answering for certain subclasses of
authorization queries.

Verifiable computation based on probabilistically checkable proofs [ALM+98] or
fully homomorphic encryption [Gen09] lacks necessary features like public
verification and their performance is currently not acceptable. In contrast,
Pinocchio is a concrete system for efficient public verification of general
computations with constant-sized proofs [PHGR13]. The applicability of non-
interactive zero-knowledge proof methods (see, for example, [MT21]) to
scalable and verifiable evidential transactions in Cyberlogic and concurrent
zero-knowledge [DNS04] needs to be investigated.

Finally, a different proposal for cryptographic proofs from the one based on
functional encryption in Section 6 implements a zero-knowledge proof of the
fact that the proof in the hand of the prover/authorizer is a correct proof of
the property in question [KFGT12]. Hereby, the property to be proven is seen
as an encryption key while the proof term is the corresponding secret key.

##  Chapter 7 Conclusions

Cyberlogic formulates a uniform semantics and logic for evidential
transactions in open-ended, large-scale, and distributed environments. Its
main concepts form the basis of a number of applications in digital
government, digital forensics, digital rights management, access control,
accountability, pervasive compliance, blockchain-based smart contracts, and
software certification. It is less clear, however, how one designs these
distributed policies and protocols systematically and correctly, so that they
can be shown to meet stated requirements, including all-important security and
privacy requirements.

Cyberlogic extends (first-order) intuitionistic logic with an attestation
modality for specifying a rich variety of services, policies, protocols, and
workflows. In this way, a number of essential features of authorization
policies such as trust, revocation, and delegation can be encoded into
Cyberlogic. Trust, for instance, is definable by the authorization
${k}\,\rhd\,{\phi}\,\Rightarrow\,\phi$, that is, we trust $\phi$ to hold
whenever principal $k$ attests to it. Moreover, temporal logic operators are
definable in Cyberlogic based on a trusted time source. Cyberlogic with its
(joint) knowledge modality and temporal logic operators therefore forms an
expressive temporal-epistemic logic [Eng96] for reasoning about distributed
policies and protocols. Another distinguishing feature is that Cyberlogic
encodings are executable, and distributed proof search is used to construct
evidence for authorizations and capabilities, which can be verified
independently. Evidence in Cyberlogic relies on its realizability semantics
and on signing direct attestations using public/private key pairs as
associated with principals. The construction and communication of explicit
proof terms, however, usually does not scale to large-scale distributed
applications. In addressing these efficiency issues we are currently
experimenting with certificate transparency111
https://sites.google.com/site/certificatetransparency/log-proofs-work/
mechanisms [Sch21], and the current implementation of ETB
Datalog222https://git.fortiss.org/evidentia/etb supports Cyberlogic-like
attestations based on IPFS.333https.io

Other requirements for a Cyberlogic interpreter include handling of failures
of the underlying communication and computation substrate, a specific
mechanism for service invocation that is richer than the interpretation of
built-in predicates [CHM+14], incremental maintenance of policies and
evidence, and modern cryptographic schemes for privacy protection. There are
solutions for each of these issues, and the challenge is to seamlessly
integrate them in a coherent and efficient Cyberlogic interpreter.

Altogether, Cyberlogic is a foundational logic for making transactions in
large-scale distributed information systems such as the Internet trustworthy
based on verifiable evidence and a small kernel of trust. Its intent is to
maximize the possibility of accountability for violations, thereby encouraging
compliance [WABL+08]. This, however, requires digital evidence to hold up to
scrutiny in real-world investigations, and it also requires a fine balance
between relevant transparency and privacy needs.

## References

  * [ABC17] Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli.  A survey of attacks on ethereum smart contracts (sok).  In International conference on principles of security and trust, pages 164--186. Springer, 2017.
  * [ABGR10] Serge Abiteboul, Meghyn Bienvenu, Alban Galland, and Marie-Christine Rousset.  Distributed datalog revisited.  In International Datalog 2.0 Workshop, pages 252--261. Springer, 2010.
  * [ABLP93] Martin Abadi, Michael Burrows, Butler Lampson, and Gordon Plotkin.  A calculus for access control in distributed systems.  ACM Transactions on Programming Languages and Systems (TOPLAS), 15(4):706--734, 1993.
  * [AF99] Andrew W Appel and Edward W Felten.  Proof-carrying authentication.  In Proceedings of the 6th ACM Conference on Computer and Communications Security, pages 52--62, 1999.
  * [AH89] James F Allen and Patrick J Hayes.  Moments and points in an interval-based temporal logic.  Computational Intelligence, 5(3):225--238, 1989.
  * [ALM+98] Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy.  Proof verification and the hardness of approximation problems.  Journal of the ACM (JACM), 45(3):501--555, 1998.
  * [And03] Scot Anderson.  Constraint datalog in trust management.  Technical report, University of Nebraska, 2003.
  * [BAP+22] Nathalie Baracaldo, Ali Anwar, Mark Purcell, Ambrish Rawat, Mathieu Sinn, Bashar Altakrouri, Dian Balta, Mahdi Sellami, Peter Kuhn, Ulrich Schopp, et al.  Towards an accountable and reproducible federated learning: A factsheets approach.  arXiv preprint arXiv:2202.12443, 2022.
  * [BC21] Tewodros A. Beyene and Carmen Carlan.  Cybergsn: A semi-formal language for specifying safety cases.  In 2021 51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W), pages 63--66, 2021.
  * [BDCG12] Andreas Blass, Guido De Caso, and Yuri Gurevich.  An introduction to dkal.  Technical report, Microsoft Research technical report, MSR-TR-2012-108, 2012.
  * [Ber06] Vincent Bernat.  First-order cyberlogic hereditary harrop logic.  Technical report, Tech. rep., SRI International, 2006.
  * [BFG10] Moritz Y Becker, Cédric Fournet, and Andrew D Gordon.  Secpal: Design and semantics of a decentralized authorization language.  Journal of Computer Security, 18(4):619--665, 2010.
  * [BFL96] Matt Blaze, Joan Feigenbaum, and Jack Lacy.  The policymaker approach to trust management.  In DIMACS Workshop on Trust Management in Networks, 1996.
  * [BGMN11] Andreas Blass, Yuri Gurevich, Michał Moskal, and Itay Neeman.  Evidential authorization.  In The Future of Software Engineering, pages 73--99. Springer, 2011\.
  * [BL19] Tim Berners-Lee.  I invented the world wide web. here’s how we can fix it.  New York Times. Erişim, 5, 2019.
  * [BSK+21] Dian Balta, Mahdi Sellami, Peter Kuhn, Ulrich Schöpp, Matthias Buchinger, Nathalie Baracaldo, Ali Anwar, Heiko Ludwig, Mathieu Sinn, Mark Purcell, et al.  Accountable federated machine learning in government: Engineering and management insights.  In International Conference on Electronic Participation, pages 125--138. Springer, 2021.
  * [BSW11] Dan Boneh, Amit Sahai, and Brent Waters.  Functional encryption: Definitions and challenges.  In Theory of Cryptography Conference, pages 253--273. Springer, 2011\.
  * [CFL+97] Yang-Hua Chu, Joan Feigenbaum, Brian LaMacchia, Paul Resnick, and Martin Strauss.  Referee: Trust management for web applications.  Computer Networks and ISDN systems, 29(8-13):953--964, 1997.
  * [CHM+14] Simon Cruanes, Stijn Heymans, Ian Mason, Sam Owre, and Natarajan Shankar.  The semantics of datalog for the evidential tool bus.  In Specification, Algebra, and Software, pages 256--275. Springer, 2014.
  * [CW18] Shumo Chu and Sophia Wang.  The curses of blockchain decentralization.  arXiv preprint arXiv:1810.02937, 2018.
  * [D+00] Michael Dummett et al.  Elements of intuitionism, volume 39.  Oxford University Press, 2000.
  * [DGP+21] David Dill, Wolfgang Grieskamp, Junkil Park, Shaz Qadeer, Meng Xu, and Emma Zhong.  Fast and reliable formal verification of smart contracts with the move prover.  arXiv preprint arXiv:2110.08362, 2021.
  * [DKTPG18] Zaynah Dargaye, Florent Kirchner, Sara Tuccı-Piergiovanni, and Onder Gürcan.  Towards secure and trusted-by-design smart contracts.  The 29th Francophone Days of Application Languages, pages 7--18, 2018.
  * [DLMS04] Nancy Durgin, Patrick Lincoln, John Mitchell, and Andre Scedrov.  Multiset rewriting and the complexity of bounded security protocols.  Journal of Computer Security, 12(2):247--311, 2004.
  * [DNS04] Cynthia Dwork, Moni Naor, and Amit Sahai.  Concurrent zero-knowledge.  Journal of the ACM (JACM), 51(6):851--898, 2004.
  * [DP01] Rowan Davies and Frank Pfenning.  A modal analysis of staged computation.  Journal of the ACM (JACM), 48(3):555--604, 2001.
  * [DPTP18] Zaynah Dargaye, Antonella Pozzo, and Sara Tucci-Piergiovanni.  Pluralize: a trustworthy framework for high-level smart contract-draft.  arXiv preprint arXiv:1812.05444, 2018.
  * [EFL+99] Carl Ellison, Bill Frantz, Butler Lampson, Ron Rivest, Brian Thomas, and Tatu Ylonen.  Spki certificate theory.  Technical report, RFC 2693, 1999.
  * [Eng96] Joeri Engelfriet.  Minimal temporal epistemic logic.  Notre Dame Journal of Formal Logic, 37(2):233--259, 1996.
  * [Fit12] Melvin Fitting.  First-order logic and automated theorem proving.  Springer Science & Business Media, 2012.
  * [FM97] Matt Fairtlough and Michael Mendler.  Propositional lax logic.  Information and Computation, 137(1):1--33, 1997.
  * [Gal15] Jean H Gallier.  Logic for computer science: foundations of automatic theorem proving.  Courier Dover Publications, 2015.
  * [GBB+06] Deepak Garg, Lujo Bauer, Kevin D Bowers, Frank Pfenning, and Michael K Reiter.  A linear logic of authorization and knowledge.  In European Symposium on Research in Computer Security, pages 297--312. Springer, 2006.
  * [GC92] David Gelernter and Nicholas Carriero.  Coordination languages and their significance.  Communications of the ACM, 35(2):96, 1992.
  * [GCS13] Ashish Gehani, Gabriela F Ciocarlie, and Natarajan Shankar.  Accountable clouds.  In 2013 IEEE International Conference on Technologies for Homeland Security (HST), pages 403--407. IEEE, 2013.
  * [Gen09] Craig Gentry.  A fully homomorphic encryption scheme.  Stanford university, 2009.
  * [GGG+14] Shafi Goldwasser, S Dov Gordon, Vipul Goyal, Abhishek Jain, Jonathan Katz, Feng-Hao Liu, Amit Sahai, Elaine Shi, and Hong-Sheng Zhou.  Multi-input functional encryption.  In Annual International Conference on the Theory and Applications of Cryptographic Techniques, pages 578--602. Springer, 2014.
  * [GKL+13] S Dov Gordon, Jonathan Katz, Feng-Hao Liu, Elaine Shi, and Hong-Sheng Zhou.  Multi-input functional encryption.  Cryptology ePrint Archive, 2013.
  * [GKS09] Ashish Gehani, Florent Kirchner, and Natarajan Shankar.  System support for forensic inference.  In IFIP International Conference on Digital Forensics, pages 301--316. Springer, 2009.
  * [GN08] Yuri Gurevich and Itay Neeman.  Dkal: Distributed-knowledge authorization language.  In 2008 21st IEEE Computer Security Foundations Symposium, pages 149--162. IEEE, 2008.
  * [GN09] Yuri Gurevich and Itay Neeman.  Dkal 2—a simplified and improved authorization language.  Technical Report MSR-TR-2009--11, 2009.
  * [GS00] Tyrone Grandison and Morris Sloman.  A survey of trust in internet applications.  IEEE Communications Surveys & Tutorials, 3(4):2--16, 2000.
  * [KFGT12] Amrit Kumar, Pierre-Alain Fouque, Thomas Genet, and Mehdi Tibouchi.  Proofs as cryptography: a new interpretation of the curry-howard isomorphism for software certificates.  HAL Open Science, 2012.
  * [Kle73] Stephen Cole Kleene.  Realizability: a retrospective survey.  In Cambridge summer school in mathematical logic, pages 95--112. Springer, 1973.
  * [LGF03] Ninghui Li, Benjamin N Grosof, and Joan Feigenbaum.  Delegation logic: A logic-based approach to distributed authorization.  ACM Transactions on Information and System Security (TISSEC), 6(1):128--171, 2003.
  * [LM03] Ninghui Li and John C Mitchell.  Datalog with constraints: A foundation for trust management languages.  In International Symposium on Practical Aspects of Declarative Languages, pages 58--73. Springer, 2003.
  * [LMS09] Peifung E Lam, John C Mitchell, and Sharada Sundaram.  A formalization of hipaa for a medical messaging system.  In International Conference on Trust, Privacy and Security in Digital Business, pages 73--85. Springer, 2009.
  * [Low96] Gavin Lowe.  Breaking and fixing the needham-schroeder public-key protocol using fdr.  In International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 147--166. Springer, 1996.
  * [Mil15] Dale Miller.  Foundational proof certificates.  All about Proofs, Proofs for All, 55:150--163, 2015.
  * [MNPS91] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov.  Uniform proofs as a foundation for logic programming.  Annals of Pure and Applied logic, 51(1-2):125--157, 1991.
  * [MR00] Jon Millen and Harald Ruess.  Protocol-independent secrecy.  In Proceeding 2000 IEEE Symposium on Security and Privacy. S&P 2000, pages 110--119. IEEE, 2000.
  * [MT21] Dimitris Mouris and Nektarios Georgios Tsoutsos.  Zilch: A framework for deploying transparent zero-knowledge proofs.  IEEE Transactions on Information Forensics and Security, 16:3269--3284, 2021.
  * [Nad93] Gopalan Nadathur.  A proof procedure for the logic of hereditary harrop formulas.  Journal of Automated Reasoning, 11(1):115--145, 1993.
  * [Nig14] Vivek Nigam.  A framework for linear authorization logics.  Theoretical Computer Science, 536:21--41, 2014.
  * [NRB+20] Vivek Nigam, Giselle Reis, Dian Balta, Tewodros Beyene, Harald Ruess, and Natarajan Shankar.  A proof theory for distributed evidential transactions.  TEASE, 2020.
  * [NRRR21] Vivek Nigam, Giselle Reis, Samar Rahmouni, and Harald Ruess.  Proof search and certificates for evidential transactions.  Automated Deduction--CADE 28, page 234, 2021.
  * [PHGR13] Bryan Parno, Jon Howell, Craig Gentry, and Mariana Raykova.  Pinocchio: Nearly practical verifiable computation.  In 2013 IEEE Symposium on Security and Privacy, pages 238--252. IEEE, 2013.
  * [PM11] Christine Paulin-Mohring.  Introduction to the coq proof-assistant for practical software verification.  In LASER Summer School on Software Engineering, pages 45--95. Springer, 2011.
  * [Rei19] Giselle Reis.  Observations about the proof theory of cyberlogic, 2019.
  * [RS03] Harald Ruess and Natarajan Shankar.  Introducing cyberlogic.  In Proceedings of the 3rd Annual High Confidence Software and Systems Conference, Baltimore, Maryland. Citeseer, 2003.
  * [RSA78] Ronald L Rivest, Adi Shamir, and Leonard Adleman.  A method for obtaining digital signatures and public-key cryptosystems.  Communications of the ACM, 21(2):120--126, 1978.
  * [Rue22] Harald Ruess.  Systems challenges for trustworthy embodied systems.  arXiv preprint arXiv:2201.03413, 2022.
  * [Sch21] Ulrich Schoepp.  Personal communication.  fortiss, 2021.
  * [WABL+08] Daniel J Weitzner, Harold Abelson, Tim Berners-Lee, Joan Feigenbaum, James Hendler, and Gerald Jay Sussman.  Information accountability.  Communications of the ACM, 51(6):82--87, 2008.
  * [ZS95] Aoying Zhou and Baile Shi.  The fixpoint characteristic of semantics of datalog with negation.  In Chinese Science Abstracts Series A, volume 5(14), page 48, 1995\.

##  Appendix A First Incarnation

The developments in this report are based on the following invited
presentation for introducing Cyberlogic at the National Security Agency’s
third High Confidence Software and Systems Conference in Baltimore, MD on
April 2003. See pages - of cyberlogic-baltimore.pdf