ISO Five-Pass Authentication protocol

Purpose

The server creates the shared key Kab and sends it to A and B. Meanwhile, B encrypts the random number with this shared key and sends it to A. A uses Kas to get Kab which then A uses to encrypt other text to be sent to B.

Informal Specification

  1. A -> B : Ra, Text1
  2. B -> S : R'b, Ra, A, Text2
  3. S -> B : Text5, E(Kbs: Kab, R'b, A, Text4), E(Kas : B, Kab, Ra, Text3)
  4. B -> A : Text7, E(Kas : B, Kab, Ra, Text3), E(Kab : Ra, Rb, Text6)
  5. A -> B : Text9, E(Kab : Ra, Rb, Text8)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 19 June 2007
--- ISO Five-Pass Authentication protocol
---     A -> B : Ra, Text1
---     B -> S : R'b, Ra, A, Text2
---     S -> B : Text5, E(Kbs: Kab, R'b, A, Text4), E(Kas : B, Kab, Ra, Text3)
---     B -> A : Text7, E(Kas : B, Kab, Ra, Text3), E(Kab : Ra, Rb, Text6)
---     A -> B : Text9, E(Kab : Ra, Rb, Text8)

(reset)
(
module ISO5pass
export * .

server : type.                         server <: princ.
key : type.
stk : princ -> princ -> type.          stk A B <: msg.  stk A B <: key.
ltk : princ -> princ -> type.          ltk A B <: key.
---assuming random nos to be nonce
nonce : type.                           nonce <: msg.
text: type.				text <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
                exists LA : nonce -> state.
IRule1:
  forall Text1 : text.
  empty
  => exists Ra : nonce.
   net(Text1 & Ra), LA Ra.

IRule5:
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Text7 : text.
   forall Text3 : text.
   forall Text6 : text.
   forall Text9 : text.
   forall Text8 : text.
   forall Ra : nonce.
   forall Rb : nonce.
    net(Text7 & enc Kas (B & Kab & Ra & Text3) & enc Kab (Ra & Rb & Text6)), LA Ra
   => net(Text9 & enc Kab (Ra & Rb & Text8)).
}


receiver:
forall B : princ.
{
                  exists LB1 : princ -> nonce -> nonce -> state.
                  exists LB2 : nonce -> nonce -> state.
IRule2:
   forall A : princ.
   forall Text1 : text.
   forall Text2 : text.
   forall Ra : nonce.
    net(Text1 & Ra)
 => exists R'b : nonce.
   net(Text2 & R'b & A & Ra), LB1 A Ra Rb.

IRule4:
   forall Text7 : text.
   forall Text3 : text.
   forall Text6 : text.
   forall Text4 : text.
   forall Text5 : text.
   forall Kab : stk A B.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Ra : nonce.
   forall R'b : nonce.
     net(Text5 & enc Kas (B & Kab & Ra & Text3) & enc Kbs (A & Kab & R'b & Text4)), LB1 A Ra Rb
  => exists Rb : nonce.
   net(Text7 & enc Kas (B & Kab & Ra & Text3) & enc Kab (Ra & Rb & Text6)), LB2 Ra Rb.


IRule6:
   forall Text9 : text.
   forall Text8 : text.
   forall Kab : stk A B.
   forall Rb : nonce.
   forall Ra : nonce.
    net(Text9 & enc Kab (Ra & Rb & Text8)), LB2 Ra Rb
   => empty.

}


server:
forall S : server.
{
IRule3:
   forall Text3 : text.
   forall Text4 : text.
   forall Text2 : text.
   forall Text5 : text.
   forall Kas : ltk A S.
   forall Kbs : ltk B S.
   forall Ra : nonce.
   forall R'b : nonce.
    net(Text2 & R'b & A & Ra)
     => exists Kab : stk A B.
        net(Text5 & enc Kas (B & Kab & Ra & Text3) & enc Kbs (A & Kab & R'b & Text4)).
}

)
 

Findings

It was found that the purpose of reconstruction was not met due to Ls because they require the exact type to be specified as it cant be derived.