Shamir Rivest Adelman Three Pass protocol

Purpose

In this protocol participants share no secrets.

Informal Specification

  1. A -> B: E(Ka : M)
  2. B -> A: E(Kb : E(Ka : M))
  3. A -> B: E(Kb : M)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 12 October 2007
--- Shamir Rivest Adelman Three Pass protocol
---      A -> B: E(Ka : M)
---      B -> A: E(Kb : E(Ka : M))
---      A -> B: E(Kb : M)
---
(reset)
(
module SRA
export * .
key : type.
ltk : princ -> type.                    ltk A <: key.
nonce : type.                           nonce <: msg.

enc : key -> msg -> msg.

net : msg -> state.

initiator:
forall A : princ.
{
		exists LA : nonce -> state.
SRule1:
  forall A : princ.
  forall Ka : ltk A.
  empty
  => exists M : nonce.
     net (enc Ka M), LA M.

SRule3:
  forall B : princ.
  forall M : nonce.
  forall Kb : ltk B.
  forall Ka : ltk A.
    net(enc Kb (enc Ka M)), LA M
   => net(enc Kb M).
}

receiver:
forall B : princ.
{
                  exists LB : nonce -> state.
SRule2:
  forall A : princ.
  forall M : nonce.
  forall Kb : ltk B.
  forall Ka : ltk A.
   net (enc Ka M)
 => net(enc Kb (enc Ka M)), LB M.

SRule4:
   forall Kb : ltk B.
   forall M : nonce.
     net(enc Kb M), LB M
  => empty.

}

)