Recently, a universally composable framework for RFID authentication protocols providing availability, anonymity, and authenticity was proposed. In this paper we extend that framework to address forward-security issues in the presence of key compromise. We also introduce new, provably secure, and highly practical protocols for anonymous authentication and key-exchange by RFID devices. The new protocols are lightweight, requiring only a pseudo-random bit generator. The new protocols satisfy forward-secure anonymity, authenticity, and availability requirements in the Universal Composability model. Categories and Subject Descriptors K.6 [Security and Protection]: Authentication; K.6 [Miscellaneous]: Security; D.2 [Software/Program verification]: Formal methods; Reliability; Validation; D.4 [Security and Protection]: Authentication; Cryptographic controls; Information flow controls; C.3 [Special-purpose and Application-based Systems]: Smartcards; C.4 [Performance of Systems]: Reliabilit...