PROTOCOL:
PBK: Purpose Built Keys Framework

VARIANT:
original version

PURPOSE:
Sender invariance (authentication assuming first message is not tampered with)
 

REFERENCE:
http://www.ietf.org/internet-drafts/draft-bradner-pbk-frame-06.txt
 

MODELER:

 

ALICE_BOB: 

  A -> B: A, PK_A, hash(PK_A)
  A -> B: {Msg}_inv(PK_A), hash(PK_A)
  B -> A: Nonce
  A -> B: {Nonce}_inv(PK_A)

 

PROBLEMS:
1
 

ATTACKS:

The initiator shall sign a random challenge received from the responder. This can easily be exploited to make agents sign whatever the intruder wishes: 
   i      -> (a,3) : start
   (a,3)  -> i     : {Msg(1)}inv(pk_a),f(pk_a)
   i      -> (a,12): start
   (a,12) -> i     : {Msg(2)}inv(pk_a),f(pk_a)
   i      -> (a,3) : x71
   (a,3)  -> i     : {x71}inv(pk_a)
   i      -> (b,3) : {x71}inv(pk_a),f(pk_a)
   (b,3)  -> i     : Nonce(4)
   i      -> (a,12): Nonce(4)
   (a,12) -> i     : {Nonce(4)}inv(pk_a)
   i      -> (b,3) : {Nonce(4)}inv(pk_a)

 

NOTES:

The protocol is so far only roughly described in natural language, and this file represents a verbatim translation to HLPSL as an ``early prototype'' and the AVISPA tool can identify a potential source for attacks which protocol designers should be aware of when implementing a protocol (see paragraph ``Attacks''). A fixed version (with tagging the challenge before signing it) is also provided in this library.

The assumption is that the intruder cannot modify (or intercept) the first message is modelled by a compression-technique. Also, the authentication must be specified in a slightly different way, as A does not say for whom it signs the message (and anybody can act as responder).

 


HLPSL: 

role alice (A,B        : agent,
            SND,RCV    : channel(dy),
            Hash       : hash_func,
            PK_A       : public_key)
played_by A
def=

  local
    State      : nat,
    Msg        : text,
    Nonce      : text

  init State := 0

  transition

 1. State  = 0 /\ RCV(start) =|>
    State':= 2 /\ Msg' := new()
               /\ SND({Msg'}_inv(PK_A).Hash(PK_A))
               /\ witness(A,A,msg,Msg')

 3. State  = 2 /\ RCV(Nonce') =|>
    State':= 4 /\ SND({Nonce'}_inv(PK_A))

end role




role bob (B,A        : agent,
          SND,RCV    : channel(dy),
          Hash       : hash_func,
          PK_A       : public_key)
played_by B
def=

  local
    State      : nat,
    Nonce      : text,
    Msg        : text

  init State := 1

  transition

 1. State  = 1 /\ RCV({Msg'}_inv(PK_A).Hash(PK_A)) =|>
    State':= 5 /\ Nonce' := new()
               /\ SND(Nonce')

 3. State  = 5 /\ RCV({Nonce}_inv(PK_A)) =|>
    State':= 7 /\ wrequest(A,A,msg,Msg)
         
end role




role session(A,B  : agent,
             Hash : hash_func,
             PK_A : public_key)
def=

  local SNDA,RCVA,SNDB,RCVB : channel (dy)

  composition

    alice(A,B,SNDA,RCVA,Hash,PK_A)
 /\ bob(B,A,SNDB,RCVB,Hash,PK_A)

end role




role environment()
def=

  const
    a,b            : agent,
    f              : hash_func,
    msg            : protocol_id,
    pk_a,pk_b,pk_i : public_key

  intruder_knowledge = {a,b,f,pk_a,pk_b,pk_i,inv(pk_i)}

  composition

     session(a,b,f,pk_a)
  /\ session(b,a,f,pk_b)
  /\ session(i,b,f,pk_i)
  /\ session(a,i,f,pk_a)

end role




goal

  % Sender Invariance (G16)
  weak_authentication_on msg

end goal




environment()