ISO Public Key Two-Pass Parallel Mutual Authentication Protocol

Purpose

Informal Specification

1. A -> B: CertA, Ra, Text1
2. B -> A: Rb, Ra, A, Text6, E(Kb-1: Rb, Ra, A, Text5)


3. B -> A: CertB, Rb, Text2
4. A -> B: Ra, Rb, B, Text4, E(Kb-1: Rb, Ra, B, Text3)

MSR Specification

--- Author: rishav
--- Date: 30 September 2007
--- ISO Public Key Two-Pass Parallel Mutual Authentication Protocol
---
---	  A -> B: CertA, Ra, Text1
---	  B -> A: Rb, Ra, A, Text6, E(Kb-1: Rb, Ra, A, Text5)

---	  B -> A: CertB, Rb, Text2
---	  A -> B: Ra, Rb, B, Text4, E(Kb-1: Rb, Ra, B, Text3)

(
module ISOTwoPassParr
export * .
key : type.
pvtk : princ -> type.          pvtk A <: key.
nonce : type.                           nonce  <: msg.
enc : key -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall A : princ.
{
			exists LA : princ -> nonce -> pvtk A -> state.
  ISO2PinitRule1:
  forall B : princ. 
  forall Ka-1 : pvtk A.
  forall text1 : text.
    empty
  => exists Ra : nonce.
     net (CertA & Ra & text1), LA B Ra Ka-1.


  ISO2PinitRule3:
  forall B : princ. 
  forall Ka-1 : pvtk A.
  forall text5 : text.
  forall text6 : text.
    net (Rb & Ra & A & text6 & enc Kb-1 (Rb & Ra & A & text5)), LA B Ra Ka-1
  => empty.
}

recicever:
forall B : princ.
{
  ISO3PinitRule2:
  forall A : princ.
  forall Kb-1 : pvtk B.
  forall text5 : text.
  forall text6 : text.
  net (CertA & Ra & text1)
  => exists Rb : nonce.
     net (Rb & Ra & A & text6 & enc Kb-1 (Rb & Ra & A & text5)).
}


initiator2:
forall B : princ.
{
				exists LB : princ -> nonce -> pvtk B -> state.
  ISO2PinitRule1:
  forall A : princ. 
  forall Kb-1 : pvtk B.
  forall text2 : text.
    empty
  => exists Rb : nonce.
     net (CertB & Rb & text2), LB A Rb Kb-1.


 ISO2PinitRule3:
  forall A : princ. 
  forall Kb-1 : pvtk B.
  forall text3 : text.
  forall text4 : text.
  forall Rb : nonce.
    net (Rb & Ra & B & text4 & enc Ka-1 (Rb & Ra & B & text3)), LB A Rb Kb-1
  => empty.


}

recicever2:
forall A : princ.
{
  ISO3PinitRule2:
  forall B : princ.
  forall Ka-1 : pvtk A.
  forall text3 : text.
  forall text4 : text.
  forall text2 : text.
  net (CertB & Rb & text2)
  => exists Ra : nonce.
     net (Rb & Ra & A & text4 & enc Ka-1 (Rb & Ra & B & text3)).
}

)