cba_bc_check_appraise_sink.md

Copland Source

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

Abstract Syntax Tree

AST n0 attest bank sys n1 @bank n1->n0 n2 appraise appraiser bank n3 {} n4 -> n4->n2 n4->n3 n5 ! n6 +<+ n6->n4 n6->n5 n7 @appraiser n7->n6 n8 -> n8->n1 n8->n7 n9 prove client id n10 @client n10->n9 n11 appraise appraiser client n12 {} n13 -> n13->n11 n13->n12 n14 ! n15 +<+ n15->n13 n15->n14 n16 @appraiser n16->n15 n17 -> n17->n10 n17->n16 n18 @bank n18->n17 n19 -<- n19->n8 n19->n18

Events and Evidence

Copland cluster_appraiser appraiser cluster_bank bank cluster_client client n47 s(mt, g(m(msp(prove, client, id), client, mt), appraiser)) n48 client: rpy(bank) n47->n48 n49 s(mt, g(m(msp(prove, client, id), client, mt), appraiser)) n48->n49 n45 s(mt, g(m(msp(prove, client, id), client, mt), appraiser)) n46 bank: rpy(appraiser) n45->n46 n46->n47 n33 bank: req(appraiser) n33->n46 n34 m(msp(prove, client, id), client, mt) n33->n34 n35 appraiser: +<+ split n34->n35 n30 m(msp(prove, client, id), client, mt) n31 bank: rpy(client) n30->n31 n32 m(msp(prove, client, id), client, mt) n31->n32 n27 bank: req(client) n27->n31 n28 mt n27->n28 n29 client: msp(prove, client, id) n28->n29 n25 client: req(bank) n25->n48 n26 mt n25->n26 n26->n27 n21 s(mt, g(m(msp(attest, bank, sys), bank, mt), appraiser)) n22 client: rpy(appraiser) n21->n22 n22->n25 n23 s(mt, g(m(msp(attest, bank, sys), bank, mt), appraiser)) n22->n23 n9 client: req(appraiser) n9->n22 n10 m(msp(attest, bank, sys), bank, mt) n9->n10 n11 appraiser: +<+ split 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 n44 appraiser: join n44->n45 n43 g(m(msp(prove, client, id), client, mt), appraiser) n43->n44 n40 mt n40->n44 n39 appraiser: nul n39->n40 n42 appraiser: sig n39->n42 n42->n43 n41 m(msp(prove, client, id), client, mt) n41->n42 n35->n41 n36 m(msp(prove, client, id), client, mt) n35->n36 n38 m(msp(appraise, appraiser, client), appraiser, m(msp(prove, client, id), client, mt)) n38->n39 n37 appraiser: msp(appraise, appraiser, client) n37->n38 n36->n37 n20 appraiser: join n20->n21 n19 g(m(msp(attest, bank, sys), bank, mt), appraiser) n19->n20 n16 mt n16->n20 n15 appraiser: nul n15->n16 n18 appraiser: sig n15->n18 n18->n19 n17 m(msp(attest, bank, sys), bank, mt) n17->n18 n11->n17 n12 m(msp(attest, bank, sys), bank, mt) n11->n12 n14 m(msp(appraise, appraiser, bank), appraiser, m(msp(attest, bank, sys), bank, mt)) n14->n15 n13 appraiser: msp(appraise, appraiser, bank) n13->n14 n12->n13 n32->n33 n5->n6 n50 client: join n51 s(s(mt, g(m(msp(attest, bank, sys), bank, mt), appraiser)),  s(mt, g(m(msp(prove, client, id), client, mt), appraiser))) n50->n51 n49->n50 n23->n50 n29->n30 n24 mt n24->n25 n1 client: -<- split n1->n24 n2 mt n1->n2 n8->n9 n2->n3 n0 mt n0->n1