A Secure Relay Protocol for Door Access Control
Resumo
Physical keys are easy to use but difficult to manage securely for large institutions. Digital replacements have been created, but dedicated hardware such as smartcards or RFID tags can have the same problems as physical keys. Several commercial products try to solve this by using the users' Bluetooth-enabled mobile devices as keys, but the built-in security of the Bluetooth standard is insufficient. Furthermore, to manage a varying set of users, such systems may require the door locks to be connected to the Internet which may require expensive infrastructure. We present a cryptographic protocol and a prototype implementation that solves these problems by letting door locks communicate with a central server using the Internet connections of the users' mobile devices. The protocol is specified formally in the applied π-calculus and security through secrecy and authenticity is verified using the cryptographic protocol verifier ProVerif. A prototype of the system is implemented for Android smartphones.
Referências
BlueLon. (2011, May 24th) BlueAccess BAL-100-BL. [Online]. Available: http://www.bluelon.com/index.php?id=248
FlexiPanel. (2007, March 1st) BlueLock - Access control triggered by Bluetooth on your mobile phone. [Online]. Available: http://www.flexipanel.com/Docs/BlueLock%20DS377%20Cover.pdf
Steab AB. (2012, January 11th) Blue Step. [Online]. Available: http://steab.se/2bluestep.html
ECKey. (2011, May 24th) ECKey - turn your phone into a key! [Online]. Available: http://www.eckey.com
SOREX - Wireless Solutions GmbH. (2012, January 11th) SOREX wireless products. [Online]. Available: http://www.sorex-austria.com/overview_wireless.html
E. R. Wognsen, H. S. Karlsen, M. Calverley, and M. N. Follin. (2011, May 27th) A proposal for a secure relay protocol for door access control. Student report at Aalborg University. [Online]. Available: http://sw8.lmz.dk/report.pdf
M. Abadi, “Private authentication,” in Proceedings of the 2nd international conference on Privacy enhancing technologies, ser. PET’02. Berlin, Heidelberg: Springer-Verlag, 2003, pp. 27–40.
M. Abadi and A. D. Gordon, “A calculus for cryptographic protocols,” Inf. Comput., vol. 148, pp. 1–70, January 1999.
B. Blanchet. (2011, December 11th) ProVerif. [Online]. Available: http://www.proverif.ens.fr
S. Kremer and M. Ryan, “Analysis of an electronic voting protocol in the applied pi calculus,” in In Proc. 14th European Symposium On Programming (ESOP’05), volume 3444 of LNCS. Springer, 2005, pp. 186–200.
K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu, “Cryptographically verified implementations for TLS,” in Proceedings of the 15th ACM conference on Computer and communications security, ser. CCS ’08. New York, NY, USA: ACM, 2008, pp. 459–468. [Online]. Available: http://doi.acm.org/10.1145/1455770.1455828
R. Chang and V. Shmatikov, “Formal analysis of authentication in bluetooth device pairing,” 2007.
B. Blanchet. (2011, December 11th) ProVerif users. [Online]. Available: http://www.proverif.ens.fr/proverif-users.html
M. Abadi and C. Fournet, “Mobile values, new names, and secure communication,” in Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ser. POPL ’01. New York, NY, USA: ACM, 2001, pp. 104–115. [Online]. Available: http://doi.acm.org/10.1145/360204.360213
R.Milner, Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, 1999.
E. R. Wognsen, H. S. Karlsen, M. Calverley, and M. N. Follin. (2012, Feb) Protocol
proverif model. [Online]. Available: http://sw8.lmz.dk/protocol.pv
Woo and S. Lam, “A semantic Model for Authentication Protocols,” in The 1993 Sym- posium on Research in Security and Privacy. IEEE Computer Society Press, May 1993, pp. 178–194.
