ISO Two-Pass Unilateral 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. B -> A: Rb,Text1
  2. A -> B: Text3, fKAB(Rb,B,Text2)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 10 December 2007
--- ISO Two-Pass Unilateral Authentication Protocol CCFs
---
---	  B -> A: Rb,Text1
---       A -> B: Text3, fKAB(Rb,B,Text2)
(reset)
(
module ISOTUA
export * .

key : type.
shrk : princ -> princ -> type.          shrk A B <: key.
randomNo: type.                           randomNo  <: msg.
f : key -> msg -> msg.
text: type.				text <: msg.

net : msg -> state.

initiator:
forall B : princ.
{
			exists LB : randomNo -> state.
  ISO2initRule1:
  forall text1 : text.
  empty
  => exists Rb : randomNo.
    net(Rb & text1), LB Rb.

 ISO2initRule3:
  forall A : princ.
  forall KaB : shrk A B.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall Rb : randomNo.
    net(text3 & f Kab (Rb & B & text2)), LB Rb
  => empty.
}

reciever:
forall A : princ.
{
  ISOinitRule2:
  forall B : princ.
  forall Kab : shrk A B.
  forall text3 : text.
  forall text2 : text.
  forall text1 : text.
  forall Rb : randomNo.
   net(Rb & text1)
  => net(text3 & f Kab (Rb & B & text2)).
}



)