PUF_weak_mutual.spthy

/******************************************************************************
 * Mutual authenticaton with weak PUFs
 *
 * check with
 * tamarin-prover --prove PUF_weak_mutual.spthy
 ******************************************************************************/

theory PUF_weak_mutual

begin

// PUF is private
functions: puf/1 [private]

builtins: hashing

/*
 * Weak Puf with 1 value: no challenge, it only outputs a fingerprint
 * Here we don't consider noise
 * NOTE 1: puf cannot depend on the server, but depends on the device, modelled as puf(D)
 * NOTE 2: We let multiple servers to store the (single) CRP. The protocol will disambiguate
 *         the server including the id in the hash
 */
rule PUF:
  [ PUFin(D) ]   --[ PUF(D)   ]-> [ PUFout(D, puf(D))   ]

rule CRP:
  [ CRPin(A,D) ] --[ CRP(A,D) ]-> [ !CRPout(A,D,puf(D)) ]

rule BreakPUF:
  [ In(D) ] --[ BreakPUF(D) ]-> [ Out(puf(D)) ]

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

/*
 * Basic hash-based device mutual authentication.
 * For strong agreement it is necessary that A is included in the hash.
 *
 * A -> D: n
 * D -> A: m,h(A,puf,n,m)
 * A -> D: h(puf,m)
 *
 * Similar to ISO/IEC 9798-4-4 but here:
 *
 * 1. A is not just for breaking simmetry, multiple A's might have valid 
 *    CRPs with D. Moreover, even if we limit CRPs to one server the device
 *    does not have a state to store this information securely. Thus it 
 *    is necessary to explicitate A so that the device can agree on that ID.
 * 2. We do not repeat A and n in the last message: this is an optimization.
 */

rule BuildWeakCRPs:
  [  ] --> [ CRPin($A,$D) ] // builds CRPs for Server-Device pairs

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

rule Alice1:
  [ Alice0(A),!CRPout(A,D,r), Fr(~n) ]
  --[  ]-> 
  [ Out(<A,D,~n>), Alice2(A,D,~n,r) ]

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

rule Don0:
  [ ] --> [ Don0($D) ]
  
rule Don1:
  [ Don0(D),In(<A,D,n>), Fr(~m) ] 
  --[ Run(D,A,<'DtoA',n,~m>) ]-> 
  [ PUFin(D), Don2(D,A,n,~m) ]

rule Don2:
  [ Don2(D,A,n,m), PUFout(D,y) ] --> 
  [ Out(<D,A,m,h(A,y,n,m)>), Don3(D,A,y,n,m) ]

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 #i #j. CRP(A,D)@i & PUF(D)@j ==> i < j"

/* 
 * The following can be useful when looking for minimal attacks on one run
 */
//restriction oneRun:
//  "All A B C D x y #i #j. Run(A,B,x)@i & Run(C,D,y)@j ==> #i = #j"

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

/*
 * Property: Secrecy of PUF with respect to A
 * with A = {BreakPUF(D), RevealCRP(a,D)}
 *
 * Intuition:
 * puf values are only leaked if CRPs are explicity revealed or 
 * if puf has been broken
 */
lemma Secrecy_A:
  "All D p #t. K(p)@t & p = puf(D) ==> 
    (Ex a #i.RevealCRP(a,D)@i & i<t ) // CRP for D is revealed by one server
    |
    (Ex #i.BreakPUF(D)@i & i<t) // PUF for D is broken
  "

/*
 * Property: Mutual authentication with respect to A
 * with A = {BreakPUF(D), RevealCRP(a,D)}
 *
 * Intuition:
 * 1) each Commit(B,C,x) is preceded by a corresponding Run(C,B,x);
 * 2) no other Commit on the same x exists.
 * unless CRPs or puf has been broken.
 *
 * Note: D in A is istantiated to C or B depending on the protocol direction
 */
lemma MutualAuthentication_A:
  "All B C x #t. Commit(B,C,x)@t ==>
  (
    (Ex #j. Run(C,B,x)@j
      & j<t 
      & not (Ex E G #k. Commit(E,G,x) @k & not (#k = #t)))
    | ( 
        (Ex n m. x = <'DtoA',n,m>) & // C is the Device
        (
          (Ex a #r. RevealCRP(a,C)@r & r<t) // It is enough that one party E that registered C reveals the CRP
            |
          (Ex #r. BreakPUF(C)@r & r<t)
        )
      )  
    | (
        (Ex n m. x = <'AtoD',n,m>) & // B is the device
        (
          (Ex a #r. RevealCRP(a,B)@r & r<t) // It is enough that one party E that registered B reveals the CRP
            |
          (Ex #r. BreakPUF(B)@r & r<t)
        )
      )   
  )
  "

end