cai_attack.spthy

/*
$tamarin-prover --prove --output-json=trace.json cai_attack.spthy
// Attack 1
==============================================================================
summary of summaries:

analyzed: cai_attack.spthy

  processing time: 0.83s

  cai_ok (all-traces): verified (2 steps)
  rac_ok (all-traces): verified (3 steps)
  completes (exists-trace): verified (6 steps)
  caught (all-traces): verified (7 steps)
  not_caught (all-traces): falsified - found trace (9 steps)

==============================================================================

// Attack 2 
==============================================================================
summary of summaries:

analyzed: cai_attack.spthy

  processing time: 101.13s

  cai_ok (all-traces): verified (2 steps)
  rac_ok (all-traces): verified (6 steps)
  completes (exists-trace): verified (30 steps)
  caught (all-traces): falsified - found trace (46 steps)
  not_caught (all-traces): verified (34 steps)

==============================================================================
*/

theory CaiAttack

begin

builtins: multiset

predicates: 
    // A ballot can only be submitted if no ballot has been submitted yet, or it has been spoiled    
    CanSubmit() <=> All p c #i #j. (Ballot(p, c) @ #i & #j = #NOW & #i < #j) ==> Ex #k.Spoil(p, c) @ #k & #k < #j,
    // Controls whether the application will submit a fake cryptogram
    Cheating() <=> Ex #i. Cheat() @ #i & #i < #NOW,
    // Ensure the traces are long enough on both sides of the fork
    Complete(plaintext, cryptogram) <=> Ex #i #j. 
        Join1(plaintext, cryptogram) @ #i & Join2(plaintext, cryptogram) @ #j

restriction OnlyOnce:
    "All #i #j. OnlyOnce()@#i & OnlyOnce()@#j ==> #i = #j"

restriction Inequality:
    "All x #i. Neq(x,x) @ #i ==> F"

// Attack 1 =================
rule Initialize:
    [  ]
  --[ OnlyOnce(), Cheat() ]->
    [ VoterSelect()]

rule AppCast:
    [ AppCast(p, c) ]
  --[ ]->
    [ Cast(p, c) ]

// ==========================

// Attack 2 =================
/*
rule Initialize:
    [  ]
  --[ OnlyOnce() ]->
    [ VoterSelect()]

rule AppCastAttack1:
    [ AppCast(p, c) ]
  --[ Spoil(p, c), Cheat()  ]->
    [ Submit(p), CastFake() ]

rule AppCastAttack2:
    [ Ballot(p, c), CastFake() ]
  --[ Join1(p, c) ]->
    [ Cast(p, c) ]
*/
// ==========================

rule VoterSelect:
    [ VoterSelect(), Fr(~p) ]
  --[ Neq(~p, 'fake') ]->
    [ Submit(~p), VoterFork() ]

rule AppSubmitBranch:
    [ Submit(p) ]
  --[ ]->
    [ SubmitHonest(p), SubmitCheat(p) ]

rule AppSubmitHonest:
    [ SubmitHonest(p) ]
  --[ _restrict(CanSubmit()), _restrict(not Cheating()), Ballot(p, p) ]->
    [ Ballot(p, p) ]

rule AppSubmitCheat:
    [ SubmitCheat(p) ]
  --[ _restrict(CanSubmit()), _restrict(Cheating()), Ballot(p, 'fake') ]->
    [ Ballot(p, 'fake') ]

rule VoterFork:
    [ Ballot(p, c), VoterFork() ]
  --[  ]->
    [ Verify(p, c), AppCast(p, c) ]

rule VerifierBranch:
    [ Verify(p, c) ]
    --[ Verify(p, c) ]->
    [ VerifyBallot1(p, c), VerifyBallot2(p, c) ]

rule VerifierOk:
    [ VerifyBallot1(p, c) ]
  --[ _restrict(c = p), CastAsIntended(p, c), Spoil(p, c), Join1(p, c) ]->
    [ 
      /*
      This accurately models the verification protocol: the voter
      can potentially cast spoil and verify forever. But this makes
      proofs impossible to complete.
      
      VoterSelect()
    */ 
  ]

rule VerifierNotOk:
    [ VerifyBallot2(p, c) ]
  --[ _restrict( not (c = p)), Caught(p, c), Spoil(p, c), Join1(p, c) ]->
    [  ]

rule BBReceipt:
    [ Cast(p, c) ]
  --[ Record(p, c) ]->
    [ Receipt(p, c) ]

rule BBVerifyReceipt:
    [ Receipt(p, c) ]
  --[ _restrict( Ex #i. Record(p, c)@ #i ), RecordedAsCast(p, c), Join2(p, c) ]->
    [ ]


lemma cai_ok:
    "All plaintext cryptogram #i. CastAsIntended(plaintext, cryptogram) @ #i
    ==> plaintext = cryptogram
    "

lemma rac_ok:
    "All plaintext cryptogram #i. RecordedAsCast(plaintext, cryptogram) @ #i
    ==> 
    Ex #j. Ballot(plaintext, cryptogram) @ #j & #j < #i
    & Ex #k. Record(plaintext, cryptogram) @ #k & #k < #i
    "

lemma completes:
    exists-trace
    "Ex plaintext cryptogram. Complete(plaintext, cryptogram)
    "

// Will be caught with some probability
lemma caught:
    "All plaintext cryptogram #i.
        RecordedAsCast(plaintext, cryptogram) @ #i & not (cryptogram = plaintext)
        & Complete(plaintext, cryptogram)
    ==> Ex #j. Caught(plaintext, cryptogram) @ #j
    "

// Will not be caught
lemma not_caught:
    "All plaintext cryptogram #i.
        RecordedAsCast(plaintext, cryptogram) @ #i & not (cryptogram = plaintext)
        & Complete(plaintext, cryptogram)
    ==> not (Ex #j. Caught(plaintext, cryptogram) @ #j)
    "

end