ISO Symmetric Key Two-Pass Mutual Authentication Protocol

Purpose

In this protocol each principal establishes that the other is operational with the help of a shared secret key. It consists of two independent uses of one-pass authentication protocol.

Informal Specification

  1. A -> B: text2, E(Kab:[Ta|Na],B,text1)
  2. B -> A: text2, E(Kab:[Tb|Nb],A,text3)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 29 May 2007
--- ISO Symmetric Key Two-Pass Mutual Authentication Protocol
---
---	  A -> B: Text2, E(Kab:[Ta|Na],B,text1)
---       B -> A: Text4, E(Kab:[Tb|Nb],A,text3)

(
module ISOTwoPassMut
export * .

shrK  : type.                             pubK <: msg.
nonce : type.                           nonce  <: msg.
enc : shrK -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall A : princ.
{
  ISO3initRule1:
  forall B : princ. 
  forall KAB : shrK.
  forall text2 : text.
  forall text1 : text.
    empty
  => exists nA : nonce.
     net (text2 & enc KAB (nA & B & text1)).
}

---they are independent
recicever:
forall B : princ.
{
  ISO3initRule2:
  forall A : princ.
  forall KAB : shrK.
  forall text3 : text.
  forall text4 : text.
   empty
  => exists nB : nonce.
     net (text4 & enc KAB (nB & A & text3)).
}

)
 

Findings