Non-termination while verifying the counter uniqueness lemma in a challenge-response protocol

[A. Y.]

Hi, I'm a bachelor's student doing a thesis on challenge response protocols with Tamarin Prover.
One of the protocols I'm trying to implement is a clone detection mechanism where the verifier can detect if the prover's secret key has been cloned.

I followed the manual, which dictates that I should use injective facts for loops that consume and reproduce the same fact. I also used heuristics for stateful protocols, as the verifier has two states (one in which it awaits the challenge and the other in which it must perform the verify).

theory 3_2_CD_Secure_Challenge
begin


builtins: signing, natural-numbers

heuristic: I


restriction Equality:
  "All x y #i. Eq(x, y) @i ==> x = y"

restriction LessThan:
  "All x y #i. LessThan(x, y) @i ==> x << y"

restriction GreaterEqualThan:
  "All x y #i. GreaterEqualThan(x, y) @i ==> not(x << y)"


/*
 * Assumptions:
 * - The protocol is based on 2_3_csa_per_verifier_keying.spthy
 * - For each (prover, verifier) pair, the prover and the verifier each maintain
 *   a counter initialized to the same value
 * - Challenges are secure, meaning the sender and recipient's identities cannot be 

 *   spoofed, and the challenge is confidential.
 *
 * Init:
 * - Each prover generates its own key pair (sk, pk)
 * - The public key is shared with the verifier
 * - Prover and verifier initialize their counters counterP and counterV
 *
 * Protocol:
 * - The verifier generates a challenge ch and sends it to the prover
 * - The prover increments its counter, and computes the response
 *   sig = sign(<counterP, ch>, sk)
 * - The prover sends sig and its incremented counter to the verifier
 * - The verifier verifies the signature verify(sig, <counterP, ch>, pk):
 *   - If true, it continues
 *   - Otherwise, it rejects it
 * - It checks that counterP <= counterV:
 *   - If true, it authenticates the prover and updates its counter
 *     counterV = counterP
 *   - Otherwise, it rejects it
 *
 * Security objective:
 * - Assuming the adversary used the cloned key to authenticate, if a cloned
 *   prover tries to authenticate, the verifier rejects the authentication
 *
 *
 */


// The secure channel is used only for the challenge.
rule secure_channel_send:
[ SecSend(A,B,m) ]
--[ SecChan_Out(A,B,m) ]->
[ Sec(A,B,m) ]
rule secure_channel_receive:
[ Sec(A,B,m) ]
--[ SecChan_In(A,B,m) ]->
[ SecRecv(A,B,m) ]


// Prover registration with the verifier:
// - Generation of a key pair
// - Sharing of the public key
// - Initialization of counters
rule Init:
    [ Fr(~sk), Fr(~pid), Fr(~vid) ]
  --[ Registers($P, $V),
      InitP(~pid, $P, $V),
      InitV(~vid, $V, $P) ]->
    [ !ProverSK($P, $V, ~sk),
      !VerifierPK($V, $P, pk(~sk)),
      StateP(~pid, $P, $V, %1),
      StateV(~vid, $V, $P, %1, 'Challenge', 'null'),
      Out(pk(~sk)) ]

// Each prover can register with a verifier only once.
restriction RegistersOnce:
  "All p v #i #j. Registers(p, v) @i & Registers(p, v) @j ==> #i = #j"

// Reveals the secret key of a prover (equivalent to cloning).
rule RevealSK:
    [ !ProverSK($P, $V, ~sk) ]
  --[ Reveal($P, $V) ]->
    [ Out(~sk) ]

// A prover can be cloned at most once.
restriction RevealOnce:
  "All p v #i #j. Reveal(p, v) @i & Reveal(p, v) @j ==> #i = #j"

// The verifier sends a challenge to the prover.
rule Challenge:
    [ StateV(~vid, $V, $P, %n_v, 'Challenge', 'null'),
      !VerifierPK($V, $P, pk),
      Fr(~ch) ]
  --[ Challenge($V, $P, ~ch),
      LoopV(~vid, $V, $P) ]->
    [ StateV(~vid, $V, $P, %n_v, 'Verify', ~ch),
      SecSend($V, $P, ~ch) ]

// The prover receives the challenge, signs it, increments its counter, and sends
// (signature, counter) to the verifier.
rule Response:
  let %next_n = %n %+ %1
      n_ch = <%next_n, ch>
      sig = sign(n_ch, ~sk)
  in
    [ SecRecv($V, $P, ch),
      StateP(~pid, $P, $V, %n),
      !ProverSK($P, $V, ~sk) ]
  --[ Responds($P, $V, n_ch),
      LoopP(~pid, $P, $V) ]->
    [ StateP(~pid, $P, $V, %next_n),
      Out(<$P, $V, n_ch, sig>) ]

// The verifier receives the signature, verifies it, and compares the counters
// successfully.
rule Verify:
  let n_ch = <n_p, ch>
  in
    [ In(<$P, $V, n_ch, sig>),
      StateV(~vid, $V, $P, %n_v, 'Verify', ch),
      !VerifierPK($V, $P, pk) ]
  --[ Verifies($V, $P, n_ch),
      Eq(verify(sig, n_ch, pk), true),
      LessThan(%n_v, n_p),
      Accepts($V, $P, n_ch),
      LoopV(~vid, $V, $P) ]->
    [ StateV(~vid, $V, $P, n_p, 'Challenge', 'null') ]

// The verifier receives the signature and verifies it successfully, but
// receives a counter greater than or equal to its local counter.
rule Detection:
  let n_ch = <n_p, ch>
  in
    [ In(<$P, $V, n_ch, sig>),
      StateV(~vid, $V, $P, %n_v, 'Verify', ch),
      !VerifierPK($V, $P, pk) ]
  --[ Verifies($V, $P, n_ch),
      Eq(verify(sig, n_ch, pk), true),
      GreaterEqualThan(%n_v, n_p),
      Detects($V, $P, n_ch),
      LoopV(~vid, $V, $P) ]->
    [ /* The verifier performs some mitigation */ ]


// ------------------------------------LEMMAS------------------------------------


// Each prover loop must have been initialized.
lemma InitBeforeLoopProver [reuse, use_induction]:
  "All p v pid #i2.
    LoopP(pid, p, v) @i2
    ==>
    (Ex #i1. InitP(pid, p, v) @i1 & #i1 < #i2)"

// Each verifier loop must have been initialized.
lemma InitBeforeLoopVerifier [reuse, use_induction]:
  "All p v vid #i2.
    LoopV(vid, v, p) @i2
    ==>
    (Ex #i1. InitV(vid, v, p) @i1 & #i1 < #i2)"

// If the verifier accepts a signature from the prover, then:
// - The same prover must have replied to the same challenge and counter
//   associated with the signature
// - There must be no further acceptances of that same challenge and counter
lemma InjectiveAgreement:
  "All p v n_ch #i2.
    Accepts(v, p, n_ch) @i2 &
    not(Ex #i. Reveal(p, v) @i)
    ==>
    (Ex #i1. Responds(p, v, n_ch) @i1 & #i1 < #i2) &
    not(Ex p_j v_j #j. Accepts(v_j, p_j, n_ch) @j & not(#j = #i2))"

// If the prover has responded to a challenge, then the verifier must have sent
// it.
// True: The challenge can't be forged nor replayed from other sessions
lemma RespondsOnlyIfChallenged:
  "All p v n_p ch #i2.
    Responds(p, v, <n_p, ch>) @i2
    ==>
    (Ex #i1. Challenge(v, p, ch) @i1 & #i1 < #i2)"

// If there was a detection, then there was a cloning.
lemma CloneDetectionSound:
  "All p v n_ch #i2.
    Detects(v, p, n_ch) @i2
    ==>
    (Ex #i1. Reveal(p, v) @i1 & #i1 < #i2)"

// After a cloning, it is always possible to detect it.
// False: the adversary chooses not to use the prover's cloned key.
lemma CloneDetectionCompleteness:
  "All p v #i1.
    Reveal(p, v) @i1
    ==>
    (Ex n_ch #i2. Detects(v, p, n_ch) @i2 & #i1 < #i2)"

lemma count_unique_prover[reuse]:
  "All p v pid n_p #i #j.
    LoopP(pid, p, v, n_p) @i & LoopP(pid, p, v, n_p) @j
    ==> #i = #j"

lemma count_unique_verifier[reuse]: // <---- Doesn't terminate
   "All p v vid n_v #i #j.
    LoopV(vid, v, p, n_v) @i & LoopV(vid, v, p, n_v) @j
    ==> #i = #j"

end

[Nik Stuckenbrock]

Hi Alessio,

I've tried to reproduce your problem in the latest version (1.12.0) of Tamarin, but I couldn't.
I proved all the lemmas automatically.

I could also solve the count_unique_verifier lemma interactively.
Are you using an older version of Tamarin, or have you attached the wrong theory?

Best,
Nik

--
You received this message because you are subscribed to the Google Groups "Tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tamarin-prover/c6b23b6b-baa2-4f27-8af9-da748ac2503dn%40googlegroups.com.

[A. Y.]

My bad, I didn't change the arity of the loop action facts which requires the actual counter value in order to prove the uniqueness.

This is the actual theory:

theory CD_Secure_Challenge

      LoopV(~vid, $V, $P, %n_v, 'Challenge') ]->

    [ StateV(~vid, $V, $P, %n_v, 'Verify', ~ch),
      SecSend($V, $P, ~ch) ]

// The prover receives the challenge, signs it, increments its counter, and sends
// (signature, counter) to the verifier.
rule Response:
  let %next_n = %n %+ %1
      n_ch = <%next_n, ch>
      sig = sign(n_ch, ~sk)
  in
    [ SecRecv($V, $P, ch),
      StateP(~pid, $P, $V, %n),
      !ProverSK($P, $V, ~sk) ]
  --[ Responds($P, $V, n_ch),

      LoopP(~pid, $P, $V, %next_n) ]->

    [ StateP(~pid, $P, $V, %next_n),
      Out(<$P, $V, n_ch, sig>) ]

// The verifier receives the signature, verifies it, and compares the counters
// successfully.
rule Verify:
  let n_ch = <n_p, ch>
  in
    [ In(<$P, $V, n_ch, sig>),
      StateV(~vid, $V, $P, %n_v, 'Verify', ch),
      !VerifierPK($V, $P, pk) ]
  --[ Verifies($V, $P, n_ch),
      Eq(verify(sig, n_ch, pk), true),
      LessThan(%n_v, n_p),
      Accepts($V, $P, n_ch),

      LoopV(~vid, $V, $P, n_p, 'Verify') ]->

    [ StateV(~vid, $V, $P, n_p, 'Challenge', 'null') ]

// The verifier receives the signature and verifies it successfully, but
// receives a counter greater than or equal to its local counter.
rule Detection:
  let n_ch = <n_p, ch>
  in
    [ In(<$P, $V, n_ch, sig>),
      StateV(~vid, $V, $P, %n_v, 'Verify', ch),
      !VerifierPK($V, $P, pk) ]
  --[ Verifies($V, $P, n_ch),
      Eq(verify(sig, n_ch, pk), true),
      GreaterEqualThan(%n_v, n_p),

      Detects($V, $P, n_ch) ]->

    [ /* The verifier performs some mitigation */ ]


// ------------------------------------LEMMAS------------------------------------


// Each prover loop must have been initialized.
lemma InitBeforeLoopProver [reuse, use_induction]:

  "All p v pid n_p #i2.
    LoopP(pid, p, v, n_p) @i2

    ==>
    (Ex #i1. InitP(pid, p, v) @i1 & #i1 < #i2)"

// Each verifier loop must have been initialized.
lemma InitBeforeLoopVerifier [reuse, use_induction]:

  "All p v vid n_v role #i2.
    LoopV(vid, v, p, n_v, role) @i2

lemma count_unique_prover[use_induction, reuse]:

  "All p v pid n_p #i #j.
    LoopP(pid, p, v, n_p) @i & LoopP(pid, p, v, n_p) @j
    ==> #i = #j"

lemma count_unique_verifier[use_induction, reuse]: // <---- Doesn't terminate
   "All p v vid n_v role #i #j.
    LoopV(vid, v, p, n_v, role) @i & LoopV(vid, v, p, n_v, role) @j
    ==> #i = #j"

end

[Kevin Milner]

Hi Alessio, this is actually quite interesting because it helped me identify a current limitation in the injectivity contradiction checking (it could establish contradictions in more general cases than it does). But, that's not super relevant to your current issue, so with that said, you can solve your issue by establishing some stricter ordering on the LoopV actions by introducing a lemma that establishes the counter always increases:

```

lemma count_increases_verify[use_induction, reuse]:
   "All p v vid %n_v %n_v2 #i #j.
    LoopV(vid, v, p, %n_v, 'Verify') @ i & LoopV(vid, v, p, %n_v2, 'Verify') @ j & #i < #j
    ==> %n_v << %n_v2"

lemma count_unique_verifier[use_induction, reuse]:
   "All p v vid %n_v role #i #j.
    LoopV(vid, v, p, %n_v, role) @i & LoopV(vid, v, p, %n_v, role) @j
    ==> #i = #j"
```
you should find that these two now autoprove.

Note I have also changed your n_v in count_unique_verifier to be the nat type (%n_v) because the count_increases_verify applies only to LoopVs where it is nat typed.

Cheers,
Kevin

[A. Y.]

Thank you very much, Dr. Milner (actually, my thesis takes inspiration from your work on the detection of the misuse of secrets).

Could you tell me the process by which you figured out that this propaedeutic lemma was needed? When I tried to prove the lemma using the GUI, I didn't find it intuitive at all.

[A. Y.]

The final lemma I'm trying to prove with the counter is the following, which also doesn't terminate:

lemma CloneDetectionInCompromisedPreviousSessions [use_induction]:
  "All p v n_ch1 n_ch2 #i2 #i3 #i4.
    Accepts(v, p, n_ch1) @i2 &
    Responds(p, v, n_ch2) @i3 &
    Verifies(v, p, n_ch2) @i4 &
    #i2 < #i3 & #i3 < #i4
    ==>
    (Ex #i1. Responds(p, v, n_ch1) @i1 & #i1 < #i2) |
    Detects(v, p, n_ch2) @i4"

If an authentication occurred at a later time i2 and the verifier successfully authenticated the prover previously at a time i1, then either the prover responded or the verifier detected cloning, i.e. the adversary obtained the prover's key to authenticate without the prover having made the response.

[Kevin Milner]

Sure, my thought process was also to begin with proving manually. I knew ultimately the proof must rely on the injectivity of the StateV(~vid, ...), because that injectivity is what prevents there from being more than one StateV with the same vid, and the way that's applied is through finding some contradictory ordering of the injective facts (i.e. you have #i's injective premise solved by #k's right hand side, and some #i < #j < #k where #j also needs the same instance of an injective fact, there's a contradiction). So I started off by clicking through solving those injective premises first just to see if there was currently a way to force some more ordering over them, or what might be the best way to add in a bit more ordering*.

Fortunately the 'Verify' role does actually already require that the counter is always increasing, so I tried proving the increasing counter lemma I posted above. Even after that though, the original lemma was still, to my surprise, still not proving; even when I was manually following through to something that looked like it should be a contradiction it was still not closing the branch. So I stared at it for a minute to try to figure out if I was blind, and then eventually realized that Tamarin didn't yet have any way to know that the counter value was always a natural number. From the way it was instantiated from the lemma action, it could have been any message term, up until you solve far enough back, and it wasn't getting there any time soon in the autoproving. So then I updated the lemma to refer specifically to the nat and was pleased to see it working.

This last point also be accomplished by changing the n_p terms in the rules themselves to be %n_p; whether this is reasonable is up to you, it is essentially enforcing the protocol will not accept a message with anything other than a natural number in that position. I think in most cases this is reasonable, since it's up to the agent what messages they accept, and one can imagine that it's easy to tell if something is a number (or, in the implementation, always interpret whatever the data is as if it were a number).

Thanks for your kind words also! I can take a look at your final lemma tomorrow when I'm back in the office. Hopefully my somewhat rambling explanation above is helpful, maybe it will give you an idea how to start tackling it in the meantime.

Cheers,

Kevin

*The brute force way to enforce a total ordering is a lemma sort of like
"All vid p v n n2 role role2 #i #j. LoopV(vid, v, p, n, role) @ i & LoopV(vid, v, p, n2, role2) @ j ==> (#i = #j) | (#i < #j) | (#j < #i)"

But this is a horribly slow approach that I don't recommend other than if you really want to chase it up manually a bit just to make sure you can hand hold it through forcing a contradictory ordering.

[A. Y.]

The lemma I sent is a proposal for a simplified scenario where only the prover has secret keys (the server does not sign).

I tried to adapt the principles of the lemma that was in your paper: "Guaranteed detection of compromise of the initiator’s key in prior sessions", which I thought it was very similar to the lemma "unmatching_implies_detect_with_one_uncompromised" in your script (counter_protocol.spthy).

----------------------------------------------------------------------------------------------------------------------------------------------------------

----------------------------------------------------------------------------------------------------------------------------------------------------------

lemma unmatching_implies_detect_with_one_uncompromised[use_induction]:
    "All pki pkr ni nr ctr #r #i niprev nrprev ctrprev #iprev.
        //Given an matching session
        ISession(pki, pkr, ni, nr, ctr) @ i & RSession(pki, pkr, ni, nr, ctr) @ r & #r < #i
        //Then for all sessions before that
        & ISession(pki, pkr, niprev, nrprev, ctrprev) @ iprev & #iprev < #i
    ==> //Either that session was also matching
        (Ex #rprev.
            RSession(pki, pkr, niprev, nrprev,ctrprev) @ rprev
                & #rprev < #iprev)
        //Or we detected
        | (Ex id #j. Detect(id, pki, pkr) @ j)
        //Or R was also compromised
        | (Ex kr #k. pk(kr) = pkr & Compromise(kr) @ k)"

----------------------------------------------------------------------------------------------------------------------------------------------------------

Is the presence of the compromise action fact on the right-hand side due to the fact that the lemma is trying to prove that "I" is able to detect the cloning of its own secret key? Because as you rightly said in your paper, following a possible misuse detection, I is not able to establish which of the two secret keys has been misused (I or R).

In my protocol it is the verifier that can detect the misuse of the prover's secret key and consequently I cannot put the action fact Reveal in my right hand side (the lemma would become trivial).