Formal verification of security protocols is a good way to show that a protocol sarisfies required security services and consequently we may trust and apply them in real world. Authentication protocols are special ones such that it is a bit difficult to show their correctness. In this paper, we consider a smart card-based remote user authentication protocol presented by Song, Korba and Yee. We verify this protocol using strand space model which is a formal verification method. In this verification we show that this protocol supply the bilateral authentication conditions according to Lowe classification.