cbaa_bc_check_appraise_sink.md

Copland Source

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

Abstract Syntax Tree

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

Events and Evidence

Copland cluster_appraiser1 appraiser1 cluster_appraiser2 appraiser2 cluster_bank bank cluster_client client n47 s(mt, g(m(msp(prove, client, id), client, mt), appraiser2)) n48 client: rpy(bank) n47->n48 n49 s(mt, g(m(msp(prove, client, id), client, mt), appraiser2)) n48->n49 n45 s(mt, g(m(msp(prove, client, id), client, mt), appraiser2)) n46 bank: rpy(appraiser2) n45->n46 n46->n47 n33 bank: req(appraiser2) n33->n46 n34 m(msp(prove, client, id), client, mt) n33->n34 n35 appraiser2: +<+ 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), appraiser1)) n22 client: rpy(appraiser1) n21->n22 n22->n25 n23 s(mt, g(m(msp(attest, bank, sys), bank, mt), appraiser1)) n22->n23 n9 client: req(appraiser1) n9->n22 n10 m(msp(attest, bank, sys), bank, mt) n9->n10 n11 appraiser1: +<+ 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 n20 appraiser1: join n20->n21 n19 g(m(msp(attest, bank, sys), bank, mt), appraiser1) n19->n20 n16 mt n16->n20 n15 appraiser1: nul n15->n16 n18 appraiser1: 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, appraiser1, bank), appraiser1, m(msp(attest, bank, sys), bank, mt)) n14->n15 n13 appraiser1: msp(appraise, appraiser1, bank) n13->n14 n12->n13 n44 appraiser2: join n44->n45 n43 g(m(msp(prove, client, id), client, mt), appraiser2) n43->n44 n40 mt n40->n44 n39 appraiser2: nul n39->n40 n42 appraiser2: 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, appraiser2, client), appraiser2, m(msp(prove, client, id), client, mt)) n38->n39 n37 appraiser2: msp(appraise, appraiser2, client) n37->n38 n36->n37 n32->n33 n5->n6 n50 client: join n51 s(s(mt, g(m(msp(attest, bank, sys), bank, mt), appraiser1)),  s(mt, g(m(msp(prove, client, id), client, mt), appraiser2))) 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