ISO Public Key Two-Pass Unilateral 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)

MSR Specification

--- Author: rishav
--- Date: 10 September 2007
--- ISO Public Key Two-Pass Unilateral Authentication Protocol
---
---	  B -> A: Rb,Text1
---       A -> B: CertA, Ra, Rb, B, Text3, E(Ka-1:Ra,Rb,B,text2)
(reset)
(
module ISOTwoPassPublicUni
export * .

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

net : msg -> state.

initiator:
forall B : princ.
{
			exists LB : {A : princ} pvtk A -> randomNo -> text -> state.
  ISO2initRule1:
  forall Ka-1 : pvtk A.
  forall text1 : text.
  empty
  => exists rB : randomNo. 
    net(rB & text1), LB A Ka-1 rB text1.

 ISO2initRule3:
  forall A : princ.
  forall Ka-1 : pvtk A.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall rB : randomNo.
  forall rA : randomNo.
    net(CertA & rA & rB & text3 & enc Ka-1 (rB & rA & B & text2)), LB A Ka-1 rB text1
  => empty.
}

reciever:
forall A : princ.
{
  ISOinitRule2:
  forall B : princ.
  forall Ka-1 : pvtk A.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall rB : randomNo.
   net(rB & text1)
  => exists CertA : msg.
     exists rA : randomNo.
     net(CertA & rA & rB & text3 & enc Ka-1 (rB & rA & B & text2)).
}



)