Download Technical Report

Then the next actor will be the set of cards contain the MiFare Classic chip, it is a little bit
different than the original MiFare Classic authentication protocol. It is shown as follows.
CardA (NT , T S) = 2b∈R (Send.A.b.U ID → Send.A.b.T S → Receive.A.b.{NR }ks1 → Send.A.b.{NT }ks2
→ Receive.A.b.{AR }ks3 → Commit.A.b.(NR , k) → Send.A.b.{AT }ks4 → STOP )
Next model will be the model of the reader. It is shown as follows.
ReaderB (NR ) = Receive.B.a.U ID → Receive.B.a.T S → Send.B.a.{NR }ks1 → Receive.B.a.{NT }ks2
→ Send.B.a.{AR }ks3 → Receive.B.a.{AT }ks4 → Commit.B.a.(NT , k) → STOP )
In the above statement of the card and the reader, a pair of commit signal means that
the actor know the communication partner is the correct partner which provide one of the
nonces that are required to create keystream 3 and 4. And it also processes the shared
sector key, and so mutual authentication can be provided by the protocol with that two
signal. In this case, we are still concerning the security properties of mutual authentication
and so we are still trying to prove the following
N ET W ORK sat Commit.A.B.(NR , k) precedes Commit.B.A.(NT , k)
or prove it by an opposite way
N ET W ORK
k
Commit.A.B.(NR ,k)
STOP sat tr |` Commit.B.A.(NT , k) = hi
Next step is the define of rank function for the theorem proving. First of all, the timestamp
choose by the tag and the UID of the tag is sent in clear, so they are assigned with positive
rank. The next thing to consider is the two signal, as we are proving the R precedes T
trace specification, so Commit.A.B.(NR ,k) is in set R and Commit.B.A.(NT ,k) is in set T.
And according to the rank function rules, Commit.B.A.(NT ,k) in set T will also have nonpositive ranking. And R will have positive ranking. The only secret in the communication
is the shared sector key, as it is not in the adversary knowledge set, so it is assigned
with non-positive ranking, all other possible keys exist in the environment is assigned
with positive ranking. Because we are now proving by contradiction and restricted the
communication to stop at R (Commit.A.B.(NR ,k)), so all other messages after it should
not appear in the environment and so all of them are assigned with a non-positive rank.
So the overall rank function is defined as follows.
ρ(T S) = 1
ρ(U ID) = 1
ρ(Commit.A.B.(NR , k)) = 1
ρ(Commit.B.A.(NT , k)) = 0
(
0,
if Key = sector key k
ρ(Key)
1,
otherwise
(
0,
if m = AT and ks = ks4
ρ({m}ks )
1,
otherwise
ρ(m1 , m2 ) = min(ρ(m1 ), ρ(m2 ))
The next step is to check the four rank function rules to see if contradiction is occurred.
For rule 1, the initial adversary knowledge set contains only all possible UID of the card
39