Semantics, languages and tools for layered attestation
As an example of a slightly different way of structuring the two unilateral attestations that make up the mutual attestation, consider the Copland phrase below. This phrase differs from the previous one in two ways:
Chiefly, we have replaced the sequential split operator +<-
connecting the appraise
and prove
subterms (in which appraise
receives input evidence and prove
does not) with the parallel
split operator -~-
in which neither operation receives input
evidence
The parentheses surrounding the entire appraise
and prove
subterm (everything on the right of the sequence operator ->
) have
been dropped
*bank: @client @bank [attest bank sys] -> appraise client bank -> {} -~- prove client id
As before, the bank requests the client request an attestation from
it. As a result of the second change, upon receiving this request,
the client issues the request to the bank and performs the prove
measurement locally on id
in parallel. The result of prove
is
“set aside” while the bank performs attest
and the client performs
appraise
on the result of attest
, exactly as before. After
sinking the result of appraise
into the {}
operator, the client
now composes mt
with the result of prove
in parallel to form the
final evidence of type
p(mt, m(msp(prove, client, id), client, mt))
Note that, except for the outermost symbol being p
(indicating
parallel rather than sequential composition), this format is identical
to that of the previous example.
This phrase maintains all of the best elements of the previous one,
including an explicit appraise
action and the desired final evidence
format. One might actually consider this phrase an improvement over
the previous one, as here the prove
measurement is taken in parallel
with the appraisal of the bank’s attestation. This highlights the
independence of the prove
result as an evidence value from any
evidence produced by these other activities.