Andrew Secure RPC Protocol

Purpose

This protocol is intended to distribute a new session key between two principals A and B. The final message contains N'B which can be used in future messages as a handshake number.

Informal Specification

  1. A -> B: A,E(Kab:Na)
  2. B -> A: E(Kab: Na+1, Nb)
  3. A -> B: E(Kab: Na+1)
  4. B -> A: E(Kab: K'ab, N'b)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 1 June 2007
---Andrew Secure RPC Protocol
---         A -> B: A,E(Kab:Na)	
---         B -> A: E(Kab: Na+1, Nb)
---         A -> B: E(Kab: Na+1)
---         B -> A: E(Kab: K'ab, N'b)
(reset)
(
module AndrewSecureRPC
export * .

key : type.
stk : princ -> princ -> type.          stk A B <: msg.  stk A B <: key.
ltk : princ -> princ -> type.          ltk A B <: key.
nonce : type.                           nonce  <: msg.

enc : key -> msg -> msg.
inc : nonce -> nonce.

net : msg -> state.

initiator:
forall A : princ.
{
	exists LA1 : nonce -> {B : princ} ltk A B -> state.
	exists LA2 : {B : princ} ltk A B -> state.

RPCRule1:
  forall B : princ.
  forall KAB : ltk A B.
    empty
  => exists nA : nonce. 
    net(A & enc KAB (nA)),
     LA1 nA B KAB.

RPCRule3:
  forall B : princ.
  forall nB : nonce.
  forall nA : nonce.
  forall KAB : ltk A B.
  net(enc KAB ((inc nA) & nB)),
---  LA1(nA, B, KAB)
     LA1 nA B KAB
  => net(enc KAB (inc nB)), LA2 B KAB.

RPCRule5:
  forall B : princ.
  forall n'B : nonce.
  forall KAB : ltk A B.
  forall K'AB : stk A B.
  net(enc KAB (K'AB & n'B)),
	LA2 B KAB
  => empty.

}


reciever:
forall B : princ.
{
	exists LB1 : nonce -> {A : princ} ltk A B -> state.

RPCRule2:
  forall A : princ.
  forall nA : nonce.
  forall nB : nonce.
  forall KAB : ltk A B.
  forall K'AB : stk A B.
    net(A & enc KAB (nA))
  => exists nB : nonce. 
     net(enc KAB ((inc nA) & nB)),
     LB1 nB A KAB.

RPCRule4:
  forall A : princ. 
  forall nB : nonce.
  forall KAB : ltk A B.
  net(enc KAB (inc NB)),
     LB1 NB A KAB
  => exists n'B : nonce.
     exists K'AB : stk A B.
     net(enc KAB (K'AB & n'B)).

}

)
 

Findings

Easy implementation of two sets of keys - long term and short term. Reconstruction works very well here.