bcb_ps_appraise_sink.md

Copland Source

*bank:
  @client @bank [attest bank sys] -> appraise client bank -> {}
          -~- prove client id

Abstract Syntax Tree

AST n0 attest bank sys n1 @bank n1->n0 n2 appraise client bank n3 {} n4 -> n4->n2 n4->n3 n5 -> n5->n1 n5->n4 n6 prove client id n7 -~- n7->n5 n7->n6 n8 @client n8->n7

Events and Evidence

Copland cluster_bank bank cluster_client client n19 p(mt, m(msp(prove, client, id), client, mt)) n20 bank: rpy(client) n19->n20 n21 p(mt, m(msp(prove, client, id), client, mt)) n20->n21 n8 m(msp(attest, bank, sys), bank, mt) n9 client: rpy(bank) n8->n9 n10 m(msp(attest, bank, sys), bank, mt) n9->n10 n5 client: req(bank) n5->n9 n6 mt n5->n6 n7 bank: msp(attest, bank, sys) n6->n7 n1 bank: req(client) n1->n20 n2 mt n1->n2 n3 client: -~- split n2->n3 n7->n8 n0 mt n0->n1 n18 client: join n18->n19 n17 m(msp(prove, client, id), client, mt) n17->n18 n14 mt n14->n18 n16 client: msp(prove, client, id) n16->n17 n15 mt n15->n16 n3->n15 n4 mt n3->n4 n13 client: nul n13->n14 n12 m(msp(appraise, client, bank), client, m(msp(attest, bank, sys), bank, mt)) n12->n13 n11 client: msp(appraise, client, bank) n11->n12 n10->n11 n4->n5