hash h

abstract ok : message
abstract ko : message.

BASIC HASH

The Basic Hash protocol as described in [A] is an RFID protocol involving:

  • a tag associated to a secret key;
  • generic readers having access to a database containing all these keys.

The protocol is as follows:

T --> R : <nT, h(nT,key)>
R --> T : ok

This file shows an incorrect attempt at proving unlinkability for Basic Hash. Unlinkability fails for the proposed system, for an irrelevant reason.

[A] Mayla Brusò, Kostas Chatzikokolakis, and Jerry den Hartog. Formal Verification of Privacy for RFID Systems. pages 75–88, July 2010.

(* In the single session system `tag(i,k)` will use `key'(i,k)`
instead of `key(i)`. *)
name key : index -> message.
name key' : index -> index -> message.

channel cT
channel cR. process tag(i:index,k:index) =
new nT;
out(cT, <nT, h(nT,diff(key(i),key'(i,k)))>).

Use diff operator to specify multiple session (left) and single session (right) roles simultaneously.

 process reader(j:index) =
in(cT,x);
try find i,k such that snd(x) = h(fst(x),diff(key(i),key'(i,k))) in
out(cR,ok)
else
out(cR,ko).

Session j of reader. For single-session version we need to find k in addition to i.

system [BasicHash] ((!_j R: reader(j)) | (!_i !_k T: tag(i,k))). System before processing:

(!_j R: reader j) | (!_i !_k T: tag i k)

System after processing:

(!_j
in(cT,x);
find (i,k) such that (snd(x) = h(fst(x),diff(key(i),key'(i,k)))) in
R: out(cR,ok); null else R1: out(cR,ko); null) |
(!_i !_k T: out(cT,pair(nT(i,k),h(nT(i,k),diff(key(i),key'(i,k))))); null)

System BasicHash registered with actions (init,R,R1,T).
 print system [BasicHash]. System [left:BasicHash/left, right:BasicHash/right]
Available actions:

action name: init
condition: true
output: empty

action name: R(j,i,k)
indices: j,i,k
condition:
snd(input@R(j,i,k)) = h(fst(input@R(j,i,k)),diff(key(i), key'(i,k)))
output: ok

action name: R1(j)
indices: j
condition:
forall (i,k:index),
not(snd(input@R1(j)) = h(fst(input@R1(j)),diff(key(i), key'(i,k))))
output: ko

action name: T(i,k)
indices: i,k
condition: true
output: <nT(i,k),h(nT(i,k),diff(key(i), key'(i,k)))>

Show the set of actions obtained from above process.

 goal [BasicHash] wa_R :
forall (tau:timestamp),
happens(tau) =>
((exists (i,k:index),
snd(input@tau) = h(fst(input@tau),diff(key(i),key'(i,k))))
<=>
(exists (i,k:index), T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) &&
snd(output@T(i,k)) = snd(input@tau))). Goal wa_R :
forall (tau:timestamp),
happens(tau) =>
(exists (i,k:index),
snd(input@tau) = h(fst(input@tau),diff(key(i), key'(i,k))))
<=>
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) &&
snd(output@T(i,k)) = snd(input@tau)

Prove wa_R as in basic-hash-wa.sp slightly modified to also hold for single-session system. The statement (or rather, its projections) is proved for both the left and right projections of the BasicHash system.

 Proof. [goal> Focused goal (1/1):
System: left:BasicHash/left, right:BasicHash/right
----------------------------------------
forall (tau:timestamp),
happens(tau) =>
(exists (i,k:index),
snd(input@tau) = h(fst(input@tau),diff(key(i), key'(i,k))))
<=>
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) &&
snd(output@T(i,k)) = snd(input@tau)

The high-level idea of the proof is to use the EUF cryptographic axiom: only the tag T(i,k) can forge h(nT(i,k),key(i)) because the secret key is not known by the attacker. Therefore, any message accepted by the reader must come from a tag that has played before. The converse implication is trivial because any honest tag output is accepted by the reader.
intro tau Hap. [> Line 81: (intro tau Hap)
[goal> Focused goal (1/1):
System: left:BasicHash/left, right:BasicHash/right
Variables: tau:timestamp
Hap: happens(tau)
----------------------------------------
(exists (i,k:index),
snd(input@tau) = h(fst(input@tau),diff(key(i), key'(i,k))))
<=>
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau)

 split => [i k Meq]. [> Line 81: (split;(intro [i k Meq]))
[goal> Focused goal (1/2):
System: left:BasicHash/left, right:BasicHash/right
Variables: i,k:index,tau:timestamp
Hap: happens(tau)
Meq: snd(input@tau) = h(fst(input@tau),diff(key(i), key'(i,k)))
----------------------------------------
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau)
+ project. [> Line 82: project
[goal> Focused goal (1/3):
System: left:BasicHash/left
Variables: i,k:index,tau:timestamp
Hap: happens(tau)
Meq: snd(input@tau) = h(fst(input@tau),key(i))
----------------------------------------
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau)

 (* Here we need to separate the proof for each projection. *)
++ euf Meq => *; by exists i,k0. [> Line 83: (((euf Meq);(intro *));by (exists i, k0))
[goal> Focused goal (1/2):
System: right:BasicHash/right
Variables: i,k:index,tau:timestamp
Hap: happens(tau)
Meq: snd(input@tau) = h(fst(input@tau),key'(i,k))
----------------------------------------
exists (i,k:index),
T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) && snd(output@T(i,k)) = snd(input@tau)
++ euf Meq => *; by exists i,k. [> Line 84: (((euf Meq);(intro *));by (exists i, k))
[goal> Focused goal (1/1):
System: left:BasicHash/left, right:BasicHash/right
Variables: i,k:index,tau:timestamp
Hap: happens(tau)
Meq: T(i,k) < tau &&
fst(output@T(i,k)) = fst(input@tau) &&
snd(output@T(i,k)) = snd(input@tau)
----------------------------------------
exists (i,k:index),
snd(input@tau) = h(fst(input@tau),diff(key(i), key'(i,k)))

 + by exists i,k. [> Line 87: by (exists i, k)
[goal> Goal wa_R is proved

For the second implication (<=), the conclusion of the goal can directly be obtained from the hypotheses.
Qed. Exiting proof mode.

Squirrel Prover

Press the left and right arrows to do and undo an instruction.

Alternatively, you can double-click on an instruction.

This zone shows a Squirrel file. You can double-click on a comment to collapse it for better readabilility.

This zone shows the output given by Squirrel.

This zone shows the output of the previous instruction, to help identifying the change caused by the instruction.

Previously: