A Simplified Digital Cash Protocol

-- The data types DATAxy are the set of data
-- that are transmitted from the principal x
-- to the principal y;
DATAcb = {tokenReq, token}
DATAcm = {responseA, responseB, goodsReq}
DATAbc = {token, badBalance, badToken,
          depositSlip, refundSlip}
DATAbm = {refundSlip, depositSlip,
          alreadyDeposited}
DATAmc = {goods, badResponse, challengeA,
          challengeB}
DATAmb = {responseA, responseB}

[Communication channels:
 as given for NetBill.]

pragma channel goodsReceived, debitC,
       depositC, depositM, mFraud, cFraud,
       mGetsRefundSlip, tokenSpent,
       mGetsToken, cKeepsToken,
       timeoutEvent, arbitration

[The consumer process CONSUMER:
 as given in the paper.]

[The merchant process MERCHANT:
 as given in the paper.]

[The bank process BANK:
 as given in the paper.]

ABORT = STOP
END = STOP
REFUND_RECEIVED = STOP
ERROR = STOP
ARBITRATION = arbitration -> STOP
NO_TRANSACTION = STOP
FRAUD_DISCOVERED = STOP

[COMM: as given for NetBill.]

-- The communication events
CIO = {| coutm, cinm, coutb, cinb |}
MIO = {| moutc, minc, moutb, minb |}
BIO = {| boutc, boutm, binc, binm |}
COMMIO = union(CIO, union(MIO, BIO))
COMMIO' = diff(COMMIO, {cinb.token})

-- The model for Money Atomicity

SYSTEM3 =
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
   \ union(COMMIO,
           {goodsReceived, mGetsRefundSlip,
            mGetsToken, tokenSpent, mFraud,
            cFraud, timeoutEvent,
            arbitration})

SYSTEMc =
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
    \ union(COMMIO',
            {goodsReceived, debitC,
             depositM, mGetsToken,
             mGetsRefundSlip, timeoutEvent,
             arbitration, mFraud, cFraud})
SYSTEMm =
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
   \ union(COMMIO,
           {goodsReceived, debitC, depositC,
            tokenSpent, cKeepsToken,
            timeoutEvent, arbitration,
            mFraud, cFraud})

SYSTEMm' = 
   ((CONSUMER [|{}|] MERCHANT [|{}|] BANK)
    [| COMMIO |] COMM)
   \ union(COMMIO,
           {goodsReceived, debitC, depositC,
            tokenSpent, cKeepsToken,
            timeoutEvent, arbitration})

SPEC3 =
   STOP |~|
   (debitC -> ((depositC -> STOP) |~|
               (cKeepsToken -> STOP) |~|
               (depositM -> STOP)))

SPECcashc =
   STOP |~|
   (cinb.token -> ((tokenSpent -> STOP) |~|
                   (cKeepsToken -> STOP) |~|
                   (depositC -> STOP)))
SPECcashm =
   STOP |~|
   (mGetsToken ->
      ((depositM-> SPECcashm) |~| 
       (mGetsRefundSlip -> SPECcashm)))

SPECcashm' =
   STOP |~|
   ((mGetsToken ->
       ((depositM-> STOP) |~| 
        (mGetsRefundSlip -> STOP)))
    |~| FRAUDM)

FRAUDM = (mGetsToken -> FRAUDM) |~|
         (mGetsRefundSlip -> FRAUDM) |~|
         (depositM -> FRAUDM) |~|
         (mFraud -> ANYM) |~|
         (cFraud -> ANYM) 

ANYM = (mGetsToken -> ANYM) |~|
       (mGetsRefundSlip -> ANYM) |~|
       (depositM -> ANYM) |~|
       (mFraud -> ANYM) |~|
       (cFraud -> ANYM) |~|
       STOP

The check of SPEC1 generated the following FDR output (and counter-example):

fdr> Check1 "SPECcashm" "SYSTEMm";
SPECcashm ....(6 states)
CONSUMER ..................(16 states)
MERCHANT ......................(24 states)
BANK .................(19 states)
COMMcm .(4 states)
COMMcb .(3 states)
COMMmc .(5 states)
COMMmb .(3 states)
COMMbc .(6 states)
COMMbm .(4 states)
readalphabet:
  Alphabet contains 4 events [up to 998]
7 configuration masks in 7 transitions
3 
6 reachable configurations         
0 
nfcompact :
  compacting 2 state normal form:
    now 2 states
174 configuration masks in 149 transitions
120 
1002 reachable configurations         
1 

SYSTEMm
Interface={|{|depositM,mGetsRefundSlip,
              mGetsToken,tick|}|}
has behaviour
After <tau,tau,tau,tau,tau,tau,tau,tau,tau,
       tau,tau,tau,tau,mGetsToken,tau,tau,
       tau,depositM,tau,tau,tau,tau,tau,
       tau,tau,tau,tau,tau,tau,mGetsToken,
       tau,tau,tau,tau,tau,tau,tau,tau,tau>
refuses {|{|depositM,mGetsRefundSlip,
            mGetsToken,tick|}|}
Accepts only {{||}|}
Contributions:
Component 1
((CONSUMER[|{||}|]MERCHANT)
 [|{||}|]BANK)
[|{|coutb,coutm,moutc,moutb,boutc, boutm,
    cinb,cinm,minc,minb,binc,binm|}|]COMM
Interface={|{|coutb,coutm,moutc,moutb,boutc,
              boutm,cinb,cinm,minc,minb,
              binc,binm,debitC,depositC,
              depositM,mFraud,cFraud,
              mGetsRefundSlip,tokenSpent,
              mGetsToken,cKeepsToken,
              timeoutEvent,arbitration,
              tick|}|}
has behaviour
After <tau,tau,coutb.tokenReq,binc.tokenReq,
       debitC,boutc.token,cinb.token,
       coutm.goodsReq,minc.goodsReq,
       moutc.challengeA,cinm.challengeA,
       coutm.responseA,minc.responseA,
       mGetsToken,moutc.goods,
       moutb.responseA,binm.responseA,
       depositM,boutm.depositSlip,
       minb.depositSlip,tau,cinm.goods,tau,
       coutm.goodsReq,minc.goodsReq,
       moutc.challengeB,cinm.challengeB,
       coutm.responseB,minc.responseB,
       mGetsToken,moutc.goods,
       moutb.responseB,binm.responseB,
       boutm.alreadyDeposited,cFraud,
       minb.alreadyDeposited,cinm.goods,tau,
       tokenSpent>
refuses {|{|coutb,coutm,moutc,moutb,boutc,
            boutm,cinb,cinm,minc,minb,binc,
            binm,debitC,depositC,depositM,
            mFraud,cFraud,mGetsRefundSlip,
            tokenSpent,mGetsToken,
            cKeepsToken,timeoutEvent,
            arbitration,tick|}|}
Accepts only {{||}|}
it = - : (label,selector,cause) Context
fdr>