/* Implementation of the Hancke-Kuhn distance bounding protocol */
/* Demonstrating the DB-secure property */

theory hk

begin

functions: h/1

// -------------------- 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 -------------------- //

  // The verifier V sends the nonce msg, as well as their own name

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

  // The prover receives a message from V, with whom he has a shared key
  // He replies by sending a nonce n of his own

rule Prover_1:
  [ Fr(~n), !Com(<m, $V>), !SharedKey($P, $V, key) ]
--[ ProverOne($P, $V, m, ~n) ]->
  [ !Com(<~n, $P>), ProverStart($P, $V, m, ~n) ]

  // The verifier sees they are talking with P, whom they share a key
  // They send a fresh challenge and signal the start of the fast phase

rule Verifier_2:
  [ Fr(~c), !Com(<n, $P>), !SharedKey($P, $V, key), VerifierStart($V, m) ]
--[ VerifierTwo($P, $V, m, n, ~c), Start() ]->
  [ !Com(~c), VerifierChallenge($P, $V, m, n, ~c) ]

  // The prover responds by sending a hash of all the nonces sent so far
  // as well as the shared key between them and V

rule Prover_2_close:
  [ !Com(c), ProverStart($P, $V, m, n), !SharedKey($P, $V, key), !AgentClose($P) ]
--[ ProverTwoClose($P, $V, m, n, c) ]->
  [ !Com(h(<key, m, n, c>)) ]

rule Prover_2_far:
  [ !Com(c), ProverStart($P, $V, m, n), !SharedKey($P, $V, key), !AgentFar($P) ]
--[ ProverTwoFar($P, $V, m, n, c), Slow() ]->
  [ !Com(h(<key, m, n, c>)) ]

  // The verifier ends the fast phase and checks everything lines up

rule Verifier_3:
  [ !Com(h(<key, m, n, c>)), !SharedKey($P, $V, key), VerifierChallenge($P, $V, m, n, c) ]
--[ VerifierComplete($P, $V, m, n, c), End() ]->
  [ ]

// ------------------- 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 )
	"

// -------------------- Sanity Check Lemmas -------------------- //
// This lemma only checks that the protocol can be executed
lemma finish_exists:
    exists-trace
  "
   ( Ex P V m n c #t #t2. (
        VerifierComplete(P, V, m, n, c)@t &
        Close(P)@t2
        )
   )
  "
  
  
// -------------------- Security protperty --------------------- //  
// If an honest Verifier V ends with an honest Prover P 
// then P must be close to him
// mafia frauds
lemma correctness:
  " 
	All P V m n c #t3. 
	VerifierComplete(P, V, m, n, c)@t3  ==>
	not(Ex #t1. Corrupt(V)@t1) ==>
	not(Ex #t2. Corrupt(P)@t2) ==>
	(Ex #t4. Close(P)@t4)
	
  "



end