cba_b_check.md

Copland Source

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

Abstract Syntax Tree

AST n0 attest bank sys n1 @bank n1->n0 n2 ! n3 @appraiser n3->n2 n4 -> n4->n1 n4->n3

Events and Evidence

Copland cluster_appraiser appraiser cluster_bank bank cluster_client client n10 g(m(msp(attest, bank, sys), bank, mt), appraiser) n11 client: rpy(appraiser) n10->n11 n12 g(m(msp(attest, bank, sys), bank, mt), appraiser) n11->n12 n7 client: req(appraiser) n7->n11 n8 m(msp(attest, bank, sys), bank, mt) n7->n8 n9 appraiser: sig n8->n9 n4 m(msp(attest, bank, sys), bank, mt) n5 client: rpy(bank) n4->n5 n6 m(msp(attest, bank, sys), bank, mt) n5->n6 n1 client: req(bank) n1->n5 n2 mt n1->n2 n3 bank: msp(attest, bank, sys) n2->n3 n9->n10 n3->n4 n6->n7 n0 mt n0->n1