ISO Symmetric Key Three-Pass Mutual Authentication Protocol

Purpose

In this protocol random numbers are used to help authentication. B checks for the presence of B and Rb in the message 2 and A checks for Ra and Rb in the message.

Informal Specification

  1. B -> A: Rb,Text1
  2. A -> B: Text3, E(Kab:Ra,Rb,B,text2)
  3. B -> A: Text5, E(Kab:Ra,Rb,text4)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 29 May 2007
--- ISO Symmetric Key Three-Pass Mutual Authentication Protocol
---  B -> A: Rb,Text1
---  A -> B: Text3, E(Kab:Ra,Rb,B,text2)
---  B -> A: Text5, E(Kab:Ra,Rb,text4)
---
(reset)
(
module ISOThreePassMutual
export * .

key : type.
shrk : princ -> princ -> type.          shrk A B <: key.
randomNo: type.                           randomNo  <: msg.

enc : key -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall B : princ.
{
  ISO4initRule1:
    forall text1 : text.
    empty
  => exists Rb : randomNo.
    net(Rb & text1).

 ISO4initRule3:
  forall A : princ.
  forall Rb : randomNo.
  forall Ra : randomNo.
  forall Kab : shrk A B.
  forall text3 : text.
  forall text2 : text.
  forall text4 : text.
  forall text5 : text.
     net(text3 & enc Kab (Rb & Ra & B & text2))
  => net(text5 & enc Kab (Rb & Ra & text4)).
}


reciever:
forall A : princ.
{
  ISO4initRule2:
  forall B : princ.
  forall Rb : randomNo.
  forall Ra : randomNo.
  forall Ka-1 : pvtk.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
   net(Rb & text1)
  =>exists Ra : randomNo. 
    net(text3 & enc Kab (Rb & Ra & B & text2)).

  ISO4initRule4:
  forall B : princ.
  forall Rb : randomNo.
  forall Ra : randomNo.
  forall text4 : text.
  forall text5 : text.
    net(text5 & enc Kab (Rb & Ra & text4))
  => empty.
}
)