PROTOCOL:

TSP: Time Stamp Protocol

PURPOSE:

Assertion of proof that a datum existed before a particular time.

REFERENCE:

RFC 3161 : http://www.faqs.org/rfcs/rfc3161.html

MODELER:

Daniel Plasto for Siemens CT IC 3, 2004

ALICE_BOB:

 C   -> TSA: Hash(Data).NonceC
 TSA -> C:   {Hash(Data).Time.NonceC}_inv(PK_TSA)

PROBLEMS:

strong authentication on authdata

ATTACKS:

None

NOTES:

The purpose of this protocol is to assert that a given datum existed before a particular time. For this a trusted time stamping authority (TSA) is used which supplies a unique time stamp. To prove this property the client checks if his datum has really been time stamped by the TSA. This is achieved by the witness/request-pair

  witness(TSA_,TSA_,authdata,Authdata')
  request(TSA_,TSA_,authdata,Authdata')

Note that we need not authenticate an agent and therefore use TSA as 1st and 2nd argument in witness/request. Actually, using instead the pair

  witness(TSA_,C,authdata,Authdata')
  request(C,TSA_,authdata,Authdata')

will yield an attack where the intruder takes a normal role and simply replays received messages.

  i -> (c,3):    start
  (c,3) -> i:    hash_(Data(1)),NonceC(1)
  i -> (tsa,10): hash_(Data(1)),NonceC(1)
  (tsa,10) -> i: {hash_(Data(1)),Time(2),NonceC(1)}inv(pk_tsa)
  i -> (c,3):    {hash_(Data(1)),Time(2),NonceC(1)}inv(pk_tsa)

  Witness tsa i authdata hash_(Data(1)),Time(2)
  Request c tsa authdata hash_(Data(1)),Time(2)

This attack does not contradict the intended property since the datum is correctly time-stamped.

HLPSL:

role client (
    C,TSA_  : agent,
    Hash    : hash_func,
    PK_TSA  : public_key,
    SND,RCV : channel)
played_by C def=

  local
    State    : nat,
    Data     : text,
    NonceC   : text,
    Time     : text

  init
    State := 0

  transition

 1. State   = 0 /\ RCV(start) =|>
    State' := 2 /\ Data' := new()
                /\ NonceC' := new()
                /\ SND(Hash(Data').NonceC')

 2. State   = 2 /\ RCV({Hash(Data).Time'.NonceC}_inv(PK_TSA)) =|>
    State' := 4

                /\ request(TSA_,TSA_,authdata,Hash(Data).Time')

end role



role tsa (
    C,TSA_     : agent,
    PK_TSA     : public_key,
    SND,RCV    : channel)
played_by TSA_ def=

  local
    State      : nat,
    HashedData : hash(text),
    NonceC     : text,
    Time       : text

  init
    State := 1

  transition

 1. State   = 1 /\ RCV(HashedData'.NonceC') =|>
    State' := 3 /\ Time' := new()
                /\ SND({HashedData'.Time'.NonceC'}_inv(PK_TSA))

                /\ witness(TSA_,TSA_,authdata,HashedData'.Time')

end role



role session (
    C,T     : agent,
    Hash    : hash_func,
    PK_TSA  : public_key)
def=

  local
     S1, S2 : channel (dy),
     R1, R2 : channel (dy)

  composition
     client(C,T,Hash,PK_TSA,S1,R1)
  /\ tsa(   C,T,     PK_TSA,S2,R2)

end role



role environment() def=

  const
    c,tsa       : agent,
    hash_       : hash_func,
    pk_tsa      : public_key,
    authdata    : protocol_id

  intruder_knowledge = {c,tsa,hash_,pk_tsa}

  composition
     session(c,tsa,hash_,pk_tsa)
  /\ session(c,tsa,hash_,pk_tsa)
  /\ session(i,tsa,hash_,pk_tsa)

end role



goal


  %TSA authenticates TSA on authdata
  authentication_on authdata

end goal



environment()