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