/* Implementation of the brands-chaum distance bounding protocol with signature */
/* Demonstrating the DB-secure property */

theory bcsigMfXOR

begin

functions: h/1, f/2

builtins: xor, symmetric-encryption, signing

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

rule Register_Keypair_close:
  [ Fr(~key) ]
--[ Once($A), Close($A), Keygen($A, ~key) ]->
  [ !Pk($A, pk(~key)), !Ltk($A, ~key), Out(pk(~key)), !AgentClose($A) ]
  
rule Register_Keypair_far:
  [ Fr(~key) ]
--[ Once($A), Far($A), Keygen($A, ~key) ]->
  [ !Pk($A, pk(~key)), !Ltk($A, ~key), Out(pk(~key)), !AgentFar($A) ]
  
rule Register_Keypair:
  [ Fr(~key) ]
--[ Once($A),Keygen($A, ~key) ]->
  [ !Pk($A, pk(~key)), !Ltk($A, ~key), Out(pk(~key)), !AgentFar($A) ]

rule Corrupt_Agent:
  [ !Ltk($A, ltk) ]
--[ Corrupt($A) ]->
  [ Out(ltk) ]
  
/*rule CommunicationOut:
	[ !Com(x) ] 
//--[ Slow() ]->
--[ ]->
	[ Out(x) ]
	
rule CommunicationIn:
	[ In(x) ] 
//--[ Slow() ]->
--[ ]->
	[ !Com(x) ]*/

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

// The prover chooses a nonce and encrypts it with a secret
// commitment key

rule Prover_1:
  [ Fr(~commit), Fr(~commitkey) ]
--[ ProverStart($Prover, ~commit, ~commitkey) ]->
  [ Out( senc(~commit, ~commitkey) ), ProverSess($Prover, ~commit, ~commitkey) ]

// The verifier acknowledges the sealed commitment, and then
// starts the fast phase with a challenge

rule Verifier_1:
  [ In( sealedcommit ), Fr(~challenge) ]
--[ VerifierCommit($V, ~challenge), Start() ]->
  [ Out(~challenge), VerifierStart(sealedcommit, ~challenge) ]

// The prover receives the challenge. They send back the
// xor of the challenge with their commit (abstracted to hash).
// They also prepare the final message which will unwrap the commit


rule Prover_2_close:
  let	response = challenge XOR commit
	msg = < challenge, response >
  in
  [ In(challenge), ProverSess($Prover, commit, commitkey), !Ltk($Prover, ltk), !AgentClose($Prover)]
--[ ProverFinish($Prover, commit, commitkey, challenge), OUTPUT(challenge, commit, challenge XOR commit) ]->
  [ Out(response), ProverPreFinal($Prover, < commitkey, sign(msg, ltk) > ) ]
  
/*rule Prover_2_far:
  let msg = < challenge, challenge XOR commit >
  in
  [ In(challenge), ProverSess($Prover, commit, commitkey), !Ltk($Prover, ltk), !AgentFar($Prover)]
--[ ProverFinish($Prover, commit, commitkey, challenge), Slow() ]->
  [ Out( challenge XOR commit ), ProverPreFinal($Prover, < commitkey, sign(msg, ltk) > ) ]*/

// The prover sends their final message

rule Prover_3:
  [ ProverPreFinal($Prover, signed_msg ) ]
--[ ]->
  [ Out(signed_msg) ]

// The verifier receives the xor of the challenge
// with some unknown value, and retreives it.

rule Verifier_2:
  [ VerifierStart(sealedcommit, challenge), In( challenge_response ) ]
--[ End() ]->
  [ VerifierPreFinal(sealedcommit, challenge, challenge_response ) ]

// The verifier receives the commit unwrapper, and checks that
// everything lines up correctly

rule Verifier_3:
  let msg_in = <commitkey, signature>
      msg = < challenge, challenge XOR commit >
      conf_sign = verify(signature, msg, pk)
  in
  [ VerifierPreFinal(senc(commit, commitkey) , commit, challenge XOR commit ), In( msg_in ),
   !Pk($Prover, pk) ]
--[ Eq(conf_sign, true), VerifierComplete($Prover, commit, challenge), Slow() ]->
  []

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

restriction at_most_once:
    "
    All A #t1 #t2. Once(A)@t1 & Once(A)@t2 ==>
        (
        #t1 = #t2
        )
    "  
    
restriction equals:
    "
    All a b #t1. Eq(a,b)@t1 ==>
    (
        a = b
    )
    "
    
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 -------------------- //
/*lemma verif2_exists:
  exists-trace
  "
    Ex Prover commit challenge #t1 #t2. (
      VerifierComplete(Prover, commit, challenge)@t1 & Close(Prover)@t2
    )
  "

lemma test [sources]:
      "
      All challenge commit response #i.
      OUTPUT(challenge, commit, response)@i 
      ==> 
      ( (Ex #j. KU(response)@j & j < i)
      | (Ex #j #k. KU(commit)@k & KU(challenge)@j & k < i & j < i )
      | (Ex P commitkey #j #k. ProverStart(P, commit, commitkey)@j & KU(challenge)@k & k < i )
      )
      "*/
 

// -------------------- Security protperty --------------------- //  
// If an honest Verifier V ends with a Prover P 
// then P must be close to him
// mafia frauds
/*lemma correctness:
  " 
	All P commit challenge #t3. 
	VerifierComplete(P, commit, challenge)@t3  ==>
	//not(Ex #t1. Corrupt(V)@t1) ==>
	not(Ex #t2. Corrupt(P)@t2) ==>
	(Ex #t4. Close(P)@t4)
	
  "*/


end