Previous  Index  Next
Send a comment
Security Protocols Open Repository
download: protocol specification in plain text
page in compressed postscript
page in pdf
page source in latex
bibTeX references


Author(s): Victor Shoup and Avi D. Rubin  (1996)

Summary: Symmetric key distribution using Smart Cards, by Shoup and Rubin.

Protocol specification (in common syntax)

A, B, S, Ca, Cb :   principal
Ka, Kb :   symkey
Kac, Kbc :   symkey
Na, Nb :   nonce
0,1,2 :   number
alias Kab = {A, 0}Kb
alias Pab = Kab + {B, 1}Ka

1.   A -> S :   A, B
2.   S -> A :   Pab, {Pab, B, 2}Ka
3.   A -> Ca :   A
4.   Ca -> A :   Na, {Na, 1, 1}Kac
5.   A -> B :   A, Na
6.   B -> Cb :   A, Na
7.   Cb -> B :   Nb, {Nb, 0, 0}Kab, {Na, Nb, 1}Kab, {Nb, 0, 1}Kab
8.   B -> A :   Nb, {Na, Nb, 1}Kab
9.   A -> Ca :   B, Na, Nb, Pab, {Pab, B, 2}Ka, {Na, Nb, 1}Kab, {Nb, 0, 1}Kab
10.   Ca -> A :   {Nb, 0, 0}Kab, {Nb, 0, 1}Kab
11.   A -> B :   {Nb, 0, 1}Kab

Description of the protocol rules


The session key {Nb, 0, 0}Kb must remain secret.


[SR96]. Some variants and implementation issues are discussed in the update [Sho96]. See also the implementor's paper [JHC+98].

Claimed proofs

The proof of [SR96] is based on the probabilistic definition of secure key distribution from Bellare and Rogaway [BR95].

[Bel01] uses a theorem proving approach, following Paulson's inductive method.


See [Sho96]. The nonce Na that A obtains from his smart card Ca must actually be truly random and not implemented by counters as first suggested in [SR96].

Indeed, if the next value of Na (sent in message 5 of session i) is predictable (let us call it Na'), then then the intruder I can query B for the verifiers including Na' (session ii) and use them to answer the next challenge of A (hence, authentication error in session iii).
i.5.   A -> B :   A, Na
ii.5.   I(A) -> B :   A, Na'
ii.6.   B -> Cb :   A, Na'
ii.7.   Cb -> B :   Nb', {Nb', 0, 0}Kab, {Na', Nb', 1}Kab, {Nb', 0, 1}Kab
ii.8.   B -> A :   Nb', {Na', Nb', 1}Kab
iii.5.   A -> I(B) :   A, Na'
iii.8.   I(B) -> A :   Nb', {Na', Nb', 1}Kab
According to [Sho96], the nonce Nb may though be a counter.


Giampaolo Bella. Mechanising a protocol for smart cards. In Proc. of e-Smart 2001, international conference on research in smart cards, LNCS. Springer-Verlag, september 2001.

Mihir Bellare and Phillip Rogaway. Provably secure session key distribution-- the three party case. In Proceedings 27th Annual Symposium on the Theory of Computing, ACM, pages 57--66, 1995.

Rob Jerdonek, Peter Honeyman, Kevin Coffman, Kim Rees, and Kip Wheeler. Implementation of a provably secure, smartcard-based key distribution protocol. In In Proceedings of the Third Smart Card Research and Advanced Application Conference, 1998.

Victor Shoup. A note on session key distribution using smart cards., july 1996.

Victor Shoup and Avi Rubin. Session key distribution using smart cards. In In Proceedings of Advances in Cryptology, EUROCRYPT'96, volume 1070 of LNCS. Springer-Verlag, 1996.
last modified 11/02/2003.
Previous  Index  Next
Send a comment