cba_bc_check.md

Copland Source

*client: @bank [attest bank sys] -> @appraiser [!]
  -<- @bank @client [prove client id] -> @appraiser !

Abstract Syntax Tree

AST n0 attest bank sys n1 @bank n1->n0 n2 ! n3 @appraiser n3->n2 n4 -> n4->n1 n4->n3 n5 prove client id n6 @client n6->n5 n7 ! n8 @appraiser n8->n7 n9 -> n9->n6 n9->n8 n10 @bank n10->n9 n11 -<- n11->n4 n11->n10

Events and Evidence

Copland cluster_appraiser appraiser cluster_bank bank cluster_client client n29 g(m(msp(prove, client, id), client, mt), appraiser) n30 client: rpy(bank) n29->n30 n31 g(m(msp(prove, client, id), client, mt), appraiser) n30->n31 n27 g(m(msp(prove, client, id), client, mt), appraiser) n28 bank: rpy(appraiser) n27->n28 n28->n29 n24 bank: req(appraiser) n24->n28 n25 m(msp(prove, client, id), client, mt) n24->n25 n26 appraiser: sig n25->n26 n21 m(msp(prove, client, id), client, mt) n22 bank: rpy(client) n21->n22 n23 m(msp(prove, client, id), client, mt) n22->n23 n18 bank: req(client) n18->n22 n19 mt n18->n19 n20 client: msp(prove, client, id) n19->n20 n16 client: req(bank) n16->n30 n17 mt n16->n17 n17->n18 n12 g(m(msp(attest, bank, sys), bank, mt), appraiser) n13 client: rpy(appraiser) n12->n13 n13->n16 n14 g(m(msp(attest, bank, sys), bank, mt), appraiser) n13->n14 n9 client: req(appraiser) n9->n13 n10 m(msp(attest, bank, sys), bank, mt) n9->n10 n11 appraiser: sig n10->n11 n6 m(msp(attest, bank, sys), bank, mt) n7 client: rpy(bank) n6->n7 n8 m(msp(attest, bank, sys), bank, mt) n7->n8 n3 client: req(bank) n3->n7 n4 mt n3->n4 n5 bank: msp(attest, bank, sys) n4->n5 n26->n27 n11->n12 n23->n24 n5->n6 n32 client: join n33 s(g(m(msp(attest, bank, sys), bank, mt), appraiser),  g(m(msp(prove, client, id), client, mt), appraiser)) n32->n33 n31->n32 n14->n32 n20->n21 n15 mt n15->n16 n1 client: -<- split n1->n15 n2 mt n1->n2 n8->n9 n2->n3 n0 mt n0->n1