PUF_strong_mutual_noisy.spthy

/******************************************************************************
 * Mutual authentication based on stong PUFs and hashes - with noise
 * It also models erasable PUFs (for the last lemma uncomment the restriction
 * that enables erasable PUFs)
 *
 * check with:
 * tamarin-prover --prove PUF_strong_mutual_noisy.spthy
 ******************************************************************************/

theory PUF_strong_mutual_noisy

begin

// PUF modelling functions are private
functions: spuf/2 [private], spufn/3 [private], gen/1, rep/2

builtins: hashing

// equational theory for removing noise
equations: rep( spufn(D,c,n) , gen( spuf(D,c)) ) = spuf(D,c)

/*
 * Strong PUF model
 *
 * This version models "noise" with a gen() function producing the helper
 * that is used to recover the correct puf(D) value
 */
rule PUFnoise:
  [ PUFin(D,c), Fr(~n) ]   --[ PUF(D,c)   ]-> [ PUFout(D, c, spufn(D,c,~n))   ]

rule CRPnoise:
  [ CRPin(A,D), Fr(~c) ] --[ CRP(A,D,~c) ]-> [ !CRPout(A,D,~c,spuf(D,~c)) ]

rule BreakPUFnoise:
  [ In(<D,c>), Fr(~n) ] --[ BreakPUF(D,c) ]-> [ Out(spufn(D,c,~n)) ]

rule RevealCRPnoise:
  [ !CRPout(A,D,c,p) ] --[ RevealCRP(A,D,c) ]-> [ Out(<c,p>) ]

// new rule for noisy PUFs
rule BreakGen:
  [ In(gen(spuf(D,c))) ] --[ BreakGen(D,c) ]-> [ Out(spuf(D,c)) ]

rule Modelling:
  [ In(<D,c,spufn(D,c1,n1)>), Fr(~n) ] --[ Model(D) ]-> [ Out(spufn(D,c,~n)) ]

/*
 * Basic hash-based device mutual authentication.
 * For strong agreement it is necessary that $A is included in the hash.
 * Either we put m and n together in message 2 and just m in message 3:
 * A -> D: c,r   ( r is the helper used to compute puf by D )
 * D -> A: m,h(A,spuf(D,c),m)
 * A -> D: h(spuf(D,c),m)
 */
rule BuildWeakCRPs:
  [  ] --> [ CRPin($A,$D) ]    // builds CRPs for Server-Device pairs

rule Alice0:
  [ ] --> [ Alice0($A) ]

rule Alice1:
  [ Alice0(A),!CRPout(A,D,c,r) ] 
  // --[ Run(A,D,<'AstartD',~n,~n>)  ]->  // used to look for minimal attacks
  --[ Start(A,D,c) ]->  
  [ Out(<A,D,c,gen(r)>), Alice2(A,D,c,r) ] // gen(r) is sent together with n

rule Alice2:
  [ Alice2(A,D,c,r), In(<D,A,m,h(A,r,m)>) ] 
  --[ Run(A,D,<'AtoD',c,m>), Commit(A,D,<'DtoA',c,m>) ]-> 
  [ Out(<A,D,h(r,m)>) ]

rule Don0:
  [ ] --> [ Don0($D) ]
  
rule Don1:
  [ Don0(D),In(<A,D,c,r>), Fr(~m) ] // r is helper value
  --[ Run(D,A,<'DtoA',c,~m>) ]-> 
  [ PUFin(D,c), Don2(D,A,c,~m,r) ] // r is passed to next state

rule Don2:
  [ Don2(D,A,c,m,r), PUFout(D,c,y) ] --> 
  [ Out(<D,A,m,h(A,rep(y,r),m)>), Don3(D,A,rep(y,r),c,m) ] // r is used to remove noise

rule Don3:
  [ Don3(D,A,y,n,m), In(<A,D,h(y,m)>) ]
  --[ Commit(D,A,<'AtoD',n,m>) ]-> 
  [ ]


// ======================================

/* 
 * Initialization is before deployment
 */
restriction resCRPbeforePUF:
  "All A D c1 c2 #i #j. CRP(A,D,c1)@i & PUF(D,c2)@j ==> i < j"

/*
 * CRPs are not reused
 */
restriction resCRPnotReuse:
  "All A D x #i #j. Run(A,D,x)@i & Run(A,D,x)@j & (Ex c r. x = <'AtoD',c,r>) ==> #i = #j"

/*
 * sanity check: the protocol can commit in both directions
 */
lemma Sanity:
  exists-trace
  "
  Ex A D c r #i. Commit(A,D,<'DtoA',c,r>)@i
  &
  Ex A D c r #i. Commit(A,D,<'AtoD',c,r>)@i
  &
  not (Ex A D c #k. RevealCRP(A,D,c)@k) 
  & 
  not (Ex D c #k. BreakPUF(D,c)@k)
  & 
  not (Ex D #k. Model(D)@k)"

/*
 * Helper lemma stating that Modeling requires another attack to 
 * intercept one PUF value. This is similar to the Secrecy_A
 * property below. Interestingly, without this lemma next proofs
 * do not converge.
 */
lemma modelPUF [use_induction, reuse]:
  "All D #t. Model(D)@t  ==> 
    (Ex c2 A #j.RevealCRP(A,D,c2)@j & j<t ) // CRP for D is revealed by one server
    |
    (Ex c #j.BreakPUF(D,c)@j & j<t) // PUF for D is broken
    |
    (Ex c #j.BreakGen(D,c)@j & j<t)
    "
    
/*
 * Property: Secrecy of PUF with respect to A
 * with A = {BreakPUF(D,c), RevealCRP(a,D,c), BreakGen(D,c)}
 *
 * Intuition:
 * puf values are only leaked if some CRP is explicity revealed or 
 * if puf has been broken.
 *
 * Note: Modelling is not possible without at least one PUF value. This
 * is why we quantify over all possibles c's
 *
 * We prove it in two steps:
 */
lemma LemmaSecrecy_A [use_induction, reuse]:
  "All D p n c #t. K(p)@t & p = spufn(D,c,n) ==> 
    (Ex c2 A #j.RevealCRP(A,D,c2)@j & j<t ) // CRP for D is revealed by one server
    |
    (Ex c #j.BreakPUF(D,c)@j & j<t) // PUF for D is broken
    |
    (Ex c #j.BreakGen(D,c)@j & j<t)
    "

lemma Secrecy_A [use_induction, reuse]:
  "All D p c #t. K(p)@t & p = spuf(D,c) ==> 
    (Ex c2 A #j.RevealCRP(A,D,c2)@j & j<t ) // CRP for D is revealed by one server
    |
    (Ex c #j.BreakPUF(D,c)@j & j<t) // PUF for D is broken
    |
    (Ex c #j.BreakGen(D,c)@j & j<t)
    "
/*
 * The following property is the same that we checked for weak PUFs!
 * We use A = {BreakPUF(D,c), RevealCRP(a,D,c), BreakGen(D,c)} as for secrecy.
 */
 lemma MutualAuthentication_A:
  "All B C x #i. Commit(B,C,x)@i ==>
  (
    (Ex #j. Run(C,B,x)@j
      & j<i 
      & not (Ex E G #k. Commit(E,G,x) @k & not (#k = #i)))
    | ( 
        (Ex n m. x = <'DtoA',n,m>) & // C is the Device
        (
          (Ex G c #r. RevealCRP(G,C,c)@r & r<i) // Need generic G if we don't add Model
            |
          (Ex c #r. BreakPUF(C,c)@r & r<i)
            |
          (Ex c #j.BreakGen(C,c)@j & j<i)
        )
      )  
    | (
        (Ex n m. x = <'AtoD',n,m>) & // B is the device
        (
          (Ex E c #r. RevealCRP(E,B,c)@r & r<i) // It is enough that one party E that registered B reveals the CRP
            |
          (Ex c #r. BreakPUF(B,c)@r & r<i)
            |
          (Ex c #j.BreakGen(B,c)@j & j<i)
        )
      ) 
  )
  "


/* 
 * This is the stronger refined property
 *
 * it holds for sets 
 * A1 = {BreakPUF(D,c), RevealCRP(a,D,c), BreakGen(D,c)}
 * A2 = {BreakPUF(D,X), RevealCRP(a,D,X), BreakGen(D,c)}
 */
lemma MutualAutentication_A1_A2:
  "All B C x y c m #t. Commit(B,C,x)@t & x = <y,c,m > ==>
  (
    (Ex #j. Run(C,B,x)@j & j<t 
      & not (Ex E F #k. Commit(E,F,x) @k & not (#k = #t)))
    | 
      ( 
        y = 'DtoA' &  // C is the Device
        (
          (
            (Ex #r. Model(C)@r & r<t)  & 
            (
              (Ex E c2 #r. RevealCRP(E,C,c2)@r & r<t ) // It is enough that one party E that registered B reveals the CRP
                |
              (Ex c2 #r. BreakPUF(C,c2)@r & r<t )
                |
              (Ex c2 #r. BreakGen(C,c2)@r & r<t )
            )
          )
          |
          (Ex  #r. RevealCRP(B,C,c)@r & r<t) // It is necessary that B revels its CRP!!!
          |
          (Ex  #k #w. w<k & k<t & Start(B,C,c)@w & BreakPUF(C,c)@k  )
          |
          (Ex  #k #w. w<k & k<t & Start(B,C,c)@w & BreakGen(C,c)@k  )

        )
      )  
    | 
      (
        y = 'AtoD' & // B is the device
        (
          (
            (Ex #r. Model(B)@r & r<t)  & 
            (
              (Ex E c2 #r. RevealCRP(E,B,c2)@r & r<t ) // It is enough that one party E that registered B reveals the CRP
                |
              (Ex c2 #r. BreakPUF(B,c2)@r & r<t )
                |
              (Ex c2 #r.BreakGen(B,c2)@r & r<t )
            )
          )
          |
              (Ex E  #r. RevealCRP(E,B,c)@r & r<t) // It is enough that one party E that registered B reveals the CRP
                |
              (Ex  #r. BreakPUF(B,c)@r & r<t)
                |
              (Ex  #r.BreakGen(B,c)@r & r<t)  

        )
      )   
  )
  "

/*
 * The following restriction implements an "erasable PUF", i.e.,
 * a PUF that never generates the same value twice
 */
restriction erasablePUF:
  "All D c #i #j. PUF(D,c)@i & PUF(D,c)@j ==> #i = #j"

/*
 * The following property holds for erasable PUF (see above)
 * When a PUF is erasable we can prove that a device will never
 * commit twice on the same challenge, preventing the 
 * possibility of CRP reuse by the attacker
 */
lemma NoChallengeReuseErasable:
  "All B C c1 c2 r1 r2 x1 x2 #i1 #i2 . 
  Commit(B,C,x1)@i1 & Commit(B,C,x2)@i2 & not(#i1=#i2) 
  &  x1 = <'AtoD', c1, r1> & x2 = <'AtoD', c2, r2>
  ==> not (c1=c2)"


end