-- intruder can't get product unless he's acting as merchant or customer
inv "inv1" (~nprod | dm | dc);

-- customer only gets product when merchant is paid
inv "inv2" (~cprod | mpay);

inv "inv3" (cprod | ~mpay);

-- honest customer eventually gets product
atl "atl1" (<< hc >> F (cprod));

-- when payment is sent, honest customer eventually gets the product
atl "atl2" (~i5 | << hc >> F (cprod));

-- exchange can be successfully completed by honest parties
atl "atl3" (<< hc, hm, hcb >> F (cprod & mpay));

-- cfair: customer fairness
-- dishonest merchant can't get paid without honest customer having a
-- strategy to get product
-- (dm should be set in n)
atl "cfair" (~(<< n >> F (npay & ~(<< hc >> F (cprod)))));

-- mfair: merchant fairness
-- dishonest customer can't get product without honest merchant having
-- a strategy to get paid
-- (dc should be set in n)
atl "mfair" (~(<< n, hcb >> F (nprod & ~(<< hm >> F (mpay)))));

-- cbal: customer balance
atl "cbal" (~(<< n, hcb >> F ((<< n >> F nprod) & ~(<< hm >> F mpay))));

-- mbal: merchant balance
atl "mbal" (~(<< n >> F ((<< n >> F npay) & ~(<< hc, hcb >> F cprod))));