ISO Symmetric Key Two-Pass Unilateral Authentication Protocol

Purpose

In this protocol principal A is authenticated by the verifier B by the means of challenge-response.

Informal Specification

  1. B -> A: Rb, text1
  2. A -> B: text3, E(Kab:Rb,B,text2)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: Rishav Bhowmick
--- Date: 28 May 2007
--- ISO Symmetric Key Two-Pass Unilateral Authentication Protocol
---
---	  B -> A: Rb,Text1
---       A -> B: Text3, E(Kab:Ra,B,text2)
(reset)
(
module ISOTwoPassUni
export * .

shrK  : type.                            
randomNo: type.                           randomNo  <: msg.
enc : shrK -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall B : princ.
{

			exists LA : randomNo. -> state.
  ISO2initRule1:
  forall text1 : text.
  empty
  => exists rB : randomNo. 
    net(rB & text1), LA rB.

 ISO2initRule3:
  forall A:princ.
  forall KAB : shrK.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall rB : randomNo.
    net(text3 & enc KAB (rB & B & text2)), LA rB
  => empty.
}

reciever:
forall A : princ.
{
  ISOinitRule2:
  forall B : princ.
  forall KAB : shrK.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall rB : randomNo.
   net(rB & text1)
  => net(text3 & enc KAB (rB & B & text2)).
}



)