/* Implementation of the Swiss-knife distance bounding protocol */
/* Demonstrating the DB-secure property for Mafia frauds */

/*
Sketch of the protocol in Alice/Bob notations:
V -> P: nV
P -> V: nP
V -> P: b
P -> V: f(b,Z0,Z1) with Z0=h1(nP,k) and Z1=xor(Z0,k)
P -> V: < h2(b,nV,nP,k),b >
*/


theory swissKnifeMF

begin

functions: f/3, h1/2, h2/4

builtins: xor

// -------------------- Tag Initialization -------------------- //

    // Rule for registering a prover/verifier. We create "agent" facts
    // Because the verifier doesn't necessarily know his communication partner
    // When he sends his first message (but we want to track V's session)
rule Register_Keypair_close:
  [ Fr(~key) ]
--[ KeyGen($A, $V, ~key) ,Once($A, $V), Close($A) ]->
  [ !SharedKey($A, $V, ~key), !AgentClose($A), !Agent($V) ]
  
rule Register_Keypair_far:
  [ Fr(~key) ]
--[ KeyGen($A, $V, ~key) ,Once($A, $V), Far($A) ]->
  [ !SharedKey($A, $V, ~key), !AgentFar($A), !Agent($V) ]


rule Corrupt_Prover:
  [ !SharedKey($A, $V, key) ]
--[ Corrupt($A) ]->
  [ Out(key) ]
  
rule Corrupt_Verifier: 
	[ !SharedKey($A,$V,key) ] 
--[ Corrupt($V) ]->
	[ Out(key)] 
	

rule CommunicationOut:
	[ !Com(x) ] 
//--[ Slow() ]->
--[]->
	[ Out(x) ]

rule CommunicationIn:
	[ In(x) ] 
//--[ Slow() ]->
--[]->
	[ !Com(x) ]

// -------------------- Protocol Rules -------------------- //

rule Verifier_1:
     [ Fr(~nV), !Agent($V) ]
--[ VerifierOne($V, ~nV),  !KU(~nV) ]->
     [ !Com(~nV), VerifierStart($V, ~nV) ]

rule Prover_1:
     [ Fr(~nP), !Com(nV), !SharedKey($P, $V, key) ]
--[ ProverOne($P, $V, nV, ~nP),  !KU(~nP) ]->
     [ !Com(~nP), ProverStart($P, $V, nV, ~nP) ]

rule Verifier_2:
     [ Fr(~c), !Com(nP), VerifierStart($V, nV) ]
--[ VerifierTwo($V, nV, nP, ~c),  !KU(~c), Start() ]->
     [ !Com(~c), VerifierChallenge($V, nV, nP, ~c) ]

rule Prover_2_close:
     let z0 = h1(nP, key)
     	 z1 = (z0 XOR key)
	 answer = f(c, z0, z1)
     in
     [ !Com(c), ProverStart($P, $V, nV, nP), !SharedKey($P, $V, key), !AgentClose($P) ]
--[ ProverTwo($P, $V, nV, nP, c), !KU(answer) ]->
     [ !Com(answer), ProverPreFinal($P, $V, nV, nP, c) ]

rule Prover_2_far:
     let z0 = h1(nP, key)
     	 z1 = (z0 XOR key)
	 answer = f(c, z0, z1)
     in
     [ !Com(c), ProverStart($P, $V, nV, nP), !SharedKey($P, $V, key), !AgentFar($P) ]
--[ ProverTwo($P, $V, nV, nP, c), !KU(answer), Slow() ]->
     [ !Com(answer), ProverPreFinal($P, $V, nV, nP, c) ]

rule Verifier_3:
     let z0 = h1(nP, key)
     	 z1 = z0 XOR k
	 answer = f(c, z0, z1)
     in
     [ !Com(answer), VerifierChallenge($V, nV, nP, c), !SharedKey($P, $V, key) ]
--[ VerifierThree($V, $P, nV, nP, c), End() ]->
     [ VerifierPreFinal($V, $P, nV, nP, c) ]

rule Prover_3:
     [ ProverPreFinal($P, $V, nV, nP, c), !SharedKey($P, $V, key) ]
--[ ProverComplete($P, $V, nV, nP, c), TagFinal(c), !KU(c) ]->
     [ !Com( < h2(c,nV,nP,key),c > ) ]

rule Verifier_4:
     let verif = < h2(c,nV,nP,key),c >
     in
     [ !Com(verif), VerifierPreFinal($V, $P, nV, nP, c), !SharedKey($P, $V, key) ]
--[ VerifierComplete($V, $P, nV, nP, c) ]->
     [ ]


// ------------------- Axioms -------------------------- //

  // A given pair of agents can only have keypair between them

restriction at_most_once:
    "
    All A V #t1 #t2. Once(A, V)@t1 & Once(A, V)@t2 ==>
        (
        #t1 = #t2
        )
    "
    
restriction one_location:
    "
    All A #t1. Close(A)@t1 ==> not(Ex #t2. Far(A)@t2)
    
    "
   
restriction one_location_bis:
    "
    All A #t1. Far(A)@t1 ==> not(Ex #t2. Close(A)@t2)
    
    "
    
restriction slow:
	"
	All #t1. Start()@t1 ==> All #t3. End()@t3 ==> All #t2. Slow()@t2 ==> not( #t1<#t2 & #t2<#t3 )
	"

lemma sources [sources]:
      "
      All c #i. 
      TagFinal(c)@i 
      ==> 
      (
      (Ex #j. KU(c)@j & j < i)
      )
      "

// -------------------- Sanity Check Lemmas -------------------- //
// This lemma only checks that the protocol can be executed
lemma finish_exists:
    exists-trace
  "
   ( Ex V P nV nP c #t #t2. (
        VerifierComplete(V, P, nV, nP, c)@t &
        Close(P)@t2
        )
   )
  "

lemma correctness:
  " 
	All P V m n c #t3. 
	VerifierComplete(V, P, m, n, c)@t3  ==>
	not(Ex #t1. Corrupt(V)@t1) ==>
	not(Ex #t2. Corrupt(P)@t2) ==>
	(Ex #t4. Close(P)@t4)
	
  "

end