R. N. Akram, P. F. Bonnefoi, S. Chaumette, K. Markantonakis, and D. Sauveron, Secure autonomous uavs fleets by using new specific embedded secure elements, 2016 IEEE Trustcom/BigDataSE/ISPA, pp.606-614, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01391817

R. N. Akram, K. Markantonakis, and K. Mayes, A paradigm shift in smart card ownership model, 2010 International Conference on Computational Science and Its Applications, pp.191-200, 2010.

, Trusted platform module for smart cards, 2014 6th International Conference on New Technologies, Mobility and Security (NTMS), pp.1-5, 2014.

, Smart Cards, European Telecommunications Standards Institute (ETSI), 2009.

Y. Gasmi, A. Sadeghi, P. Stewin, M. Unger, and N. Asokan, Beyond Secure Channels, STC '07: Proceedings of the 2007 ACM workshop on Scalable trusted computing, pp.30-40, 2007.

, Trusted platform module main specification, Trusted Computing Group, 2011.

L. Zhou and Z. Zhang, Trusted Channels with Password-Based Authentication and TPM-Based Attestation, Communications and Mobile Computing, International Conference on, vol.1, pp.223-227, 2010.

F. Armknecht, Y. Gasmi, A. Sadeghi, P. Stewin, M. Unger et al., An efficient implementation of trusted channels based on openssl, Proceedings of the 3rd ACM workshop on Scalable trusted computing, ser. STC '08, pp.41-50, 2008.

R. N. Akram, K. Markantonakis, and K. Mayes, A Privacy Preserving Application Acquisition Protocol, 11th IEEE International Conference on Trust, Security and Privacy in Computing and Communications, 2012.

O. Blazy, P. Bonnefoi, E. Conchon, D. Sauveron, R. N. Akram et al., An efficient protocol for uas security, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01610409

J. A. Steinmann, R. F. Babiceanu, and R. Seker, Uas security: Encryption key negotiation for partitioned data, 2016 Integrated Communications Navigation and Surveillance (ICNS), pp.1-4, 2016.

D. F. Pigatto, L. Gonçalves, G. F. Roberto, J. F. Rodrigues-filho, N. B. Floro-da-silva et al., The hamster data communication architecture for unmanned aerial, ground and aquatic systems, Journal of Intelligent & Robotic Systems, vol.84, issue.1, pp.705-723, 2016.

J. A. Maxa, M. S. Mahmoud, and N. Larrieu, Extended verification of secure uaanet routing protocol, 2016 IEEE/AIAA 35th Digital Avionics Systems Conference (DASC), pp.1-16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01365933

J. Won, S. Seo, and E. Bertino, A secure communication protocol for drones and smart objects, Proceedings of the 10th ACM Symposium on Information, Computer and Communications Security, ser. ASIA CCS '15, pp.249-260, 2015.

T. Dierks and E. Rescorla, RFC 5246-The Transport Layer Security (TLS) Protocol Version 1.2, Tech. Rep, 2008.

W. Diffie, P. C. Van-oorschot, and M. J. Wiener, Authentication and Authenticated Key Exchanges, Designs, Codes and Cryptography, vol.2, issue.2, pp.107-125, 1992.

A. Aziz and W. Diffie, Privacy And Authentication For Wireless Local Area Networks, IEEE Personal Communications, vol.1, pp.25-31, 1994.

, Authentication and payment in future mobile systems," ser. Lecture Notes in Computer Science, vol.1485, pp.277-293, 1998.

W. Aiello, S. M. Bellovin, M. Blaze, R. Canetti, J. Ioannidis et al., Just fast keying: Key agreement in a hostile internet, ACM Trans. Inf. Syst. Secur, vol.7, pp.242-273, 2004.

, Remote Application Management over HTTP, Card Specification v 2.2-Amendment B, Online, GlobalPlatform Specification, 2006.

K. Markantonakis and K. Mayes, A Secure Channel Protocol for Multi-application Smart Cards based on Public Key Cryptography, CMS 2004-Eight IFIP TC6-11 Conference on Communications and, pp.79-96, 2004.
DOI : 10.1007/11382324_6
URL : https://link.springer.com/content/pdf/10.1007%2F0-387-24486-7_6.pdf

W. G. Sirett, J. A. Macdonald, K. Mayes, and C. Markantonakis, Smart Card Research and Advanced Applications, 7th IFIP WG 8.8/11.2 International Conference, CARDIS, ser, vol.3928, pp.1-15, 2006.

S. Blake-wilson, D. Johnson, and A. Menezes, Key Agreement Protocols and Their Security Analysis, Proceedings of the 6th IMA International Conference on Cryptography and Coding, pp.30-45, 1997.
DOI : 10.1007/bfb0024447
URL : http://www.cacr.math.uwaterloo.ca/techreports/1997/corr97-17.ps

C. Mitchell, M. Ward, and P. Wilson, Key Control in Key Agreement Protocols, Electronics Letters, vol.34, issue.10, pp.980-981, 1998.

A. J. Menezes, P. C. Van-oorschot, and S. A. Vanstone, Handbook of Applied Cryptography. CRC, 1996.

C. Furlani, Online, National Institute of Standards and Technology (NIST) Std, FIPS 186-3 : Digital Signature Standard (DSS), 2009.

R. N. Akram, K. Markantonakis, and K. Mayes, A Dynamic and Ubiquitous Smart Card Security Assurance and Validation Mechanism, pp.161-172, 2010.
URL : https://hal.archives-ouvertes.fr/hal-01054520

G. Lowe, Casper: a compiler for the analysis of security protocols, J. Comput. Secur, vol.6, pp.53-84, 1998.

C. A. Hoare, Communicating sequential processes, vol.21, 1978.

P. Ryan and S. Schneider, The Modelling and Analysis of Security Protocols: the CSP Approach, 2000.

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The avispa tool for the automated validation of internet security protocols and applications, Proceedings of the 17th International Conference on Computer Aided Verification, ser. CAV'05, pp.281-285, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000408

, State=0 /\ RCV(start) =|> State':=2 /\ NS1':= new() /\ Rs1' := new

, {SIGN(Sdata2')}_(inv(PK2')).{SIGN(Svalid2')}_(inv(PKTM2'))

. Mac(ka, {{SIGN(Sdata2')}_(inv(PK2'))

, }_(inv(PKTM2')).CSE2'.CTMSE2'}_Ke') .VR2.Scookie) =|>, {SIGN(Svalid2')

, = 4 /\ SAS1':= new() /\ Svalid1':= SAS1'.NS2'.NS1

/. Sdata1, Rs2').exp(G, Rs1).NS2'.NS1)

/. Kdh, Rs1) /\ Ke':= {Hk(NS1.NS2'.1)}_Kdh' /\ Ka':= {Hk

, {SIGN(Svalid1')}_(inv(PKTM1)).MAC(Ka'. {{SIGN(Sdata1')}_(inv(PK1))

, {SIGN(Svalid1')}_(inv(PKTM1)).CSE1.CTMSE1}_Ke').Scookie)

, Success') =|> State':=6 /\ request (A,B, ns2, NS2) /\ secret (Kdh,sec_kdh1, {A,B}) /\ secret(Ke, sec_ke1, {A,B}) /\ secret

, Rs1'). VR1.Scookie) =|> State':= 3 /\ NS2':= new() /\ Rs2':=new() /\ SAS2':= new

/. Sdata2,

/. Svalid2,

/. Ke, = {Hk(NS1.NS2'.1)}_Kdh' /\ Ka' := {Hk

, {SIGN(Sdata2')}_(inv(PK2)). {SIGN(Svalid2')}

. Mac(ka, {{SIGN(Sdata2')}_(inv(PK2))

, {SIGN(Svalid2')}_(inv(PKTM2)).CSE2.CTMSE2}_Ke').VR2.Scookie)

, {SIGN(Svalid1')}_(inv(PKTM1')).MAC(Ka.{{SIGN(Sdata1')}_(inv(PK1'))

, {SIGN(Svalid1')}_(inv(PKTM1')).CSE1'.CTMSE1'}_Ke).Scookie) =|> State':= 5 /\ request