ISO Public Key Three-Pass Mutual Authentication Protocol

Purpose

Informal Specification

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

MSR Specification

--- Author: rishav
--- Date: 16 September 2007
--- ISO Three-Pass Mutual Authentication Protocol
---
---	  B -> A: Rb,Text1
---       A -> B: CertA, Ra, Rb, B, Text3, E(Ka-1:Ra,Rb,B,text2)
---       B -> A: CertB, Rb, Ra, A, Text5, E(Kb-1:Rb,Ra,A,text4)
(reset)
(
module ISOPublicThreePassMutual
export * .

key : type.
skey : type.
pvtk : princ -> type.          pvtk A <: key.
randomNo: type.                           randomNo  <: msg.

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

net : msg -> state.

initiator:
forall B : princ.
{
 		exists LB : randomNo -> state.

 ISO3initRule1:
    forall text1 : text.
    empty
  => exists Rb : randomNo.
    net(Rb & text1), LB Rb.

 ISO3initRule3:
  forall A : princ.
  forall Rb : randomNo.
  forall Ra : randomNo.
  forall Ka-1 : pvtk.
  forall text3 : text.
  forall text2 : text.
  forall text4 : text.
  forall text5 : text.
     net(CertA & Ra & Rb & B & text3 & enc Ka-1 (Rb & Ra & B & text2)), LB Rb
  => net(CertB & Rb & Ra & A & text5 & enc Kb-1 (Rb & Ra & A & text4)).
}


reciever:
forall A : princ.
{
				exists LA : princ -> randomNo -> randomNo -> state.
  ISO3initRule2:
  forall B : princ.
  forall Rb : randomNo.
  forall Ka-1 : pvtk.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
   net(Rb & text1)
  =>exists Ra : randomNo. 
    net(CertA & Ra & Rb & B & text3 & enc Ka-1 (Rb & Ra & B & text2)), LA B Ra Rb.

  ISO3initRule4:
  forall B : princ.
  forall Rb : randomNo.
  forall Ra : randomNo.
  forall text4 : text.
  forall text5 : text.
    net(CertB & Rb & Ra & A & text5 & enc Kb-1 (Rb & Ra & A & text4)), LA B Ra Rb
  => empty.
}
)