Using Non-reversible function

Purpose

The protocol allows the principal to generate a new session key K. B checks the value of f(Rb) and then sends f(Ra) encrypted with K sent by A which A checks if it is correct or not.

Informal Specification

  1. B -> A: B,Rb
  2. A -> B: A, E(Kab:f(Rb),Ra,A,K)
  3. B -> A: B, E(K:f(Ra))

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 29,30 May 2007
--- Using Non-reversible function
---
---	  B -> A: B,Rb
---       A -> B: A, E(Kab:f(Rb),Ra,A,K)
---       B -> A: B, E(K:f(Ra))
(reset)
(
module nonRevFunc
export * .

shrK  : type.                             shrK <: msg.
randomNo: type.                           randomNo  <: msg.
enc : shrK -> msg -> msg.
f : randomNo -> msg.

net : msg -> state.

initiator:
forall B : princ.
{
                  exists LA : randomNo -> princ -> state.
  revFuncRule1:
  forall A : princ.
   empty
  => exists rB : randomNo. 
    net(rB & B), LA rB B.


 revFuncRule3:
  forall A : princ.
  forall rB : randomNo.
  forall rA : randomNo.
  forall K : shrK.
 net(A & enc KAB (f rB & rA & A & K)), LA rB B
  => net(B & enc K (f rA)).
}

reciever:
forall A : princ.
{
			exists LB : randomNo -> princ -> state.
  revFuncRule2:
  forall B : princ.
  forall rB : randomNo.
   net(rB & B)
  => exists K : shrK.
     exists rA : randomNo.
     net(A & enc KAB (f rB & rA & A & K)), LB rA A.


 revFuncRule4:
  forall B : princ.
  forall rB : randomNo.
  forall rA : randomNo.
  net(B & enc K (f rA)), LB rA A
  => empty.
}


)
 

Findings

After declaring the function f, while encrypting the random number with a key, MSR implementation demanded a set of parantheses.