SPLICE/AS authentication Protocol

Purpose

We assume that initially, the client C and the server S only know their own public and private key, and that the authority AS knows everyone's public key. E(Kas-1: AS, C, N1, Ks) (in message 2) and E(Kas-1 : AS, S, N3, Kc) (in message 5) are certificates signed and distributed by the authority AS, for the respective public keys Ks and Kc. After a successfull run of the protocol, the value of N2 can be used by C and S as a symmetric key for secure communications.

Informal Specification

  1. C -> AS : C, S, N1
  2. AS -> C : AS, E(Kas-1 : AS, C, N1, Ks)
  3. C -> S : C, S, E(Kc-1 : C, T, L E(Ks:N2))
  4. S -> AS : S, C, N3
  5. AS -> S : AS, E(Kas-1 : AS, S, N3, Kc)
  6. S -> C : S, C, E(Kc: S, N2+1)

See Commonly Used Representations

MSR Specification

Click here to download 
--- Author: rishav
--- Date: 11 October 2007
--- SPLICE/AS authentication Protocol
---     C -> AS : C, S, N1
---     AS -> C : AS, E(Kas-1 : AS, C, N1, Ks) 
---     C -> S : C, S, E(Kc-1 : C, T, L E(Ks:N2))
---     S -> AS : S, C, N3
---     AS -> S : AS, E(Kas-1 : AS, S, N3, Kc)
---     S -> C : S, C, E(Kc: S, N2+1)
(reset)
(
module SPLICE
export * .

server : type.                         server <: princ.
CA : type.                             CA <: princ.
key : type.
ltk : princ -> type.          ltk A <: key.          ltk A <: msg.
ltks : princ -> type.		       ltks S <: key. 
nonce : type.                         nonce <: msg.

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


initiator:
forall C : princ.
{
			exists LC : princ -> nonce -> state.
			exists LC2 : princ -> nonce -> state.
SPRule1:
   forall S : server.
   empty
  => exists N1 : nonce. 
     net(C & S & N1), LC S N1.

SPRule3:
   forall AS : CA.
   forall S : server.
   forall Kas-1 : ltks AS.
   forall Ks : ltk S.
   forall Kc-1 : ltks C.
   forall Ks : ltk S.
   forall N1 : nonce.
   forall T : msg.
   forall L : msg.
   net(AS & enc Kas-1 (AS & C & N1 & Ks)), LC S N1
   => exists N2 : nonce.
      net(C & S & enc Kc-1 (C & T & L & enc Ks N2)), LC S N2.

SPRule7:
   forall S : server.
   forall N2 : nonce.
   forall Kc : ltk C.
    net(S & C & enc Kc (S & inc N2)), LC S N2
  => empty.


}

receiver:
forall AS : CA.
{
			exists LAS : princ -> princ -> state.
SPRule2:
   forall S : server.
   forall Kas-1 : ltks AS.
   forall Ks : ltk S.
   forall N1 : nonce.
     net(C & S & N1)
  => net(AS & enc Kas-1 (AS & C & N1 & Ks)), LAS S AS.


SPRule5:
   forall C : princ.
   forall S : server.
   forall N3 : nonce.
   forall Kas-1 : ltks AS.
   forall Kc : ltk C.
     net(S & C & N3), LAS S AS
   => net(AS & enc Kas-1 (AS & S & N3 & Kc)).

}


server:
forall S : server.
{
			exists LS : princ -> princ -> nonce -> state.
SPRule4:
   forall C : princ.
   forall AS : CA.
   forall S : server.
   forall Kas-1 : ltks AS.
   forall Kc-1 : ltks C. 
   forall Ks : ltk S.
   forall N2 : nonce.
   forall T : msg.
   forall L : msg.
    net(C & S & enc Kc-1 (C & T & L & enc Ks N2)) 
   => exists N3 : nonce.
      net(S & C & N3), LS C AS N3.

SPRule6:
   forall AS : CA.
   forall C : princ.
   forall N3 : nonce.
   forall N2 : nonce.
   forall Kas-1 : ltks AS.
   forall Kc : ltk C.
     net(AS & enc Kas-1 (AS & S & N3 & Kc)), LS C AS N3
  => net(S & C & enc Kc (S & inc N2)).

}


)