ISO Symmetric Key One-Pass Unilateral Authentication Protocol

Purpose

This protocol consists of a single message from A to B while sharing a secret key Kab.

Informal Specification

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

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: Rishav Bhowmick
--- Date: 27 May 2007
--- ISO Symmetric Key One-Pass Unilateral Authentication Protocol
---
---       A -> B: Text2, E(Kab:[Ta|Na],B,text1)
(reset)
(
module ISOOnePassUni
export * .

---msg : type.

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

net : msg -> state.

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


receiver:
forall B : princ.
{
  ISORecRule2:
  forall A : princ. 
  forall KAB : shrK.
  forall text2 : text.
  forall text1 : text.
    net (text2 & enc KAB (NA & B & text1))
  => empty.
}

)