theory TLS 
begin

builtins: hashing, symmetric-encryption, asymmetric-encryption, signing

section{* TLS Handshake *}

/*
 * Protocol:	TLS Handshake
 * Modeler: 	Simon Meier, minor update by Cas Cremers
 * Date: 	January 2012
 * Source:	Modeled after Paulson`s TLS model in Isabelle/src/HOL/Auth/TLS.thy.
 *
 * Status: 	working (2.5 seconds on an i7 Quad-Core CPU with +RTS -N)
 */

text{*
  Modeled after Paulson`s TLS model in Isabelle/src/HOL/Auth/TLS.thy. Notable
  differences are:

    1. We use explicit global constants to differentiate between different
       encryptions instead of implicit typing.

    2. We model session keys directly as hashes of the relevant information.
       Due to our support for composed keys, we do not need any custom
       axiomatization as Paulson does.

*}

functions: PRF/1

// Public key infrastructure
rule Register_pk:
  [ Fr(~ltkA) ] 
  --> 
  [ !Ltk($A, ~ltkA), !Pk($A, pk(~ltkA)), Out(pk(~ltkA)) ]

rule Reveal_ltk:
  [ !Ltk(A, ltkA) ] --[ RevLtk(A)    ]-> [ Out(ltkA) ]


/* We formalize the following signature based TLS handshake.

  protocol TLS {
    1. C -> S: C, nc, sid, pc
    2. C <- S: ns, sid, ps

    3. C -> S: { '31', pms                     }pk(S) ,
               sign{ '32', h('32', ns, S, pms) }pk(C) ,
               { '33', sid, PRF(pms, nc, ns),
                 nc, pc, C, ns, ps, S
               } 
               h('clientKey', nc, ns, PRF(pms, nc, ns))

    4. C <- S: { '4', sid, PRF(pms, nc, ns),
                 nc, pc, C, ns, ps, S
               } 
               h('serverKey', nc, ns, PRF(pms, nc, ns))
  }
*/

rule C_1:
    [ Fr(~nc)
    , Fr(~sid)
    ]
  --[]->
    [ Out(
        <$C, ~nc, ~sid, $pc>
      )
    , St_C_1($C, ~nc, ~sid, $pc)
    ]

rule S_1:
    [ In( 
        <$C, nc, sid, pc>
      )
    , Fr(~ns)
    ]
  --[]->
    [ Out(
        <$S, ~ns, sid, $ps>
      )
    , St_S_1($S, $C, sid, nc, pc, ~ns, $ps)
    ]

rule C_2:
  let 
      MS   = PRF(~pms, nc, ns)
      Ckey = h('clientKey', nc, ns, MS)
  in 
    [ St_C_1(C, nc, sid, pc)
    , In(
        <S, ns, sid, ps>
      )
    , Fr(~pms)
    , !Pk(S, pkS)
    , !Ltk(C, ltkC)
    ]
  --[]->
    [ Out(
        < aenc{ '31', ~pms }pkS
        , sign{ '32', h('32', ns, S, ~pms) }ltkC
        , senc{ '33', sid, MS, nc, pc, C, ns, ps, S}Ckey
        >
      )
    , St_C_2(S, C, sid, nc, pc, ns, ps, ~pms)
    ]

rule S_2:
  let 
      MS   = PRF(pms, nc, ns)
      Ckey = h('clientKey', nc, ns, MS)
      Skey = h('serverKey', nc, ns, MS)
  in 
    [ St_S_1(S, C, sid, nc, pc, ns, ps)
    , In(
        < aenc{ '31', pms }pk(ltkS)
        , signature
        , senc{ '33', sid, MS, nc, pc, C, ns, ps, S}Ckey
        >
      )
    , !Pk(C, pkC)
    , !Ltk(S, ltkS)
    ]
    /* Explicit equality check, enforced as part of the property. */
  --[ Eq(verify(signature, <'32', h('32', ns, S, pms)>, pkC), true )
    , SessionKeys( S, C, Skey, Ckey )
    ]->
    [ Out(
        senc{ '4', sid, MS, nc, pc, C, ns, ps, S}Skey
      )
    ]

rule C_3:
  let 
      MS   = PRF(pms, nc, ns)
      Ckey = h('clientKey', nc, ns, MS)
      Skey = h('serverKey', nc, ns, MS)
  in 
    [ St_C_2(S, C, sid, nc, pc, ns, ps, pms)
    , In( senc{ '4', sid, MS, nc, pc, C, ns, ps, S}Skey )
    ]
  --[ SessionKeys( S, C, Skey, Ckey ) ]->
    []


/* TODO: Also model session-key reveals and adapt security properties. */


/* Session key secrecy from the perspecitive of both the server and the client
 * for both the key of the server and the key of the client. Note that this
 * lemma thus captures four security properties at once. */
lemma session_key_secrecy:
  " /* If all equality checks succeeded */
    (All x y #i. Eq(x,y) @ i ==> x = y)
  ==>
    /* then there is no attack */ 
    (not( 
         /* It cannot be that */
         Ex S C keyS keyC #k.
           /* somebody claims to have setup session keys, */
           SessionKeys(S, C, keyS, keyC) @ k 
           /* but the adversary knows one of them */
         & ( (Ex #i. K(keyS) @ i) 
           | (Ex #i. K(keyC) @ i)
           )
           /* without having performed a long-term key reveal. */
         & not (Ex #r. RevLtk(S) @ r)
         & not (Ex #r. RevLtk(C) @ r)
    )   )"

/* Consistency check: this lemma must NOT have a proof,
 * as otherwise no session-keys could be setup between honest agents. */
lemma session_key_setup_possible:
  exists-trace
  " /* There is a trace satisfying all equality checks */
     (All x y #i. Eq(x,y) @ i ==> x = y)
  &  /* Session keys have been setup */
     (Ex S C keyS keyC #k.  SessionKeys(S, C, keyS, keyC) @ k 
      /* without having performed a long-term key reveal. */
      & not (Ex #r. RevLtk(S) @ r)
      & not (Ex #r. RevLtk(C) @ r)
      )
   "


end