ISO Two-Pass Mutual Authentication Protocol with CCFs (Cryptographic Check Functions)

Purpose

The keyed function fKab(X) returns hashed value for data X in a manner determined by the key Kab.

Informal Specification

  1. A -> B: [Ta|Na], Text2, fKab([Ta|Na],B,text1)
  2. B -> A: [Ta|Na], Text4, fKab([Tb|Nb],A,text3)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 11 December 2007
--- ISO Two-Pass Mutual Authentication Protocol  CCFs
---
---	  A -> B: [Ta|Na], Text2, fKab([Ta|Na],B,text1)
---       B -> A: [Ta|Na], Text4, fKab([Tb|Nb],A,text3)

(
module ISOTMA
export * .
key : type.
shrk : princ -> princ -> type.          shrk A B <: key.
nonce : type.                           nonce  <: msg.
f : key -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall A : princ.
{
  ISO2initRule1:
  forall B : princ. 
  forall Kab : shrk A B.
  forall text2 : text.
  forall text1 : text.
    empty
  => exists Na : nonce.
     net (Na & text2 & f Kab (Na & B & text1)).
}

---they are independent
recicever:
forall B : princ.
{
  ISO2initRule2:
  forall A : princ.
  forall Kab : shrk A B.
  forall text3 : text.
  forall text4 : text.
   empty
  => exists Nb : nonce.
     net (Nb & text4 & f Kab (Nb & A & text3)).
}

)