, B_i selection and verification of key PuK.RCA.AUT by
, AUT key, and then returns the confirma- tion
, CS_AUT and returnt it to the MU.A
, CS_AUT, saves the public key PuK.CASP.A.CS_AUT and sends confirmation to the MU.A: SP.B_i -> MU.B_i -> MU.A: conf.OK 3 MU.A through MU.B_i requests SP.B_i to choose and verify the key PuK, CS_AUT: MU.A -> MU.B_i -> SP.B_i: select and verify(PuK.CASP.A.CS_AUT)
, CS_AUT key, and then returns the confir- mation: SP.B_i -> MU.B_i -> MU.A: conf.OK 5 MU.A asks SP.A to read its authentication certificate C, SP.A.AUT: MU.A -> SP.A: get certificate (C.SP.A.AUT)
, AUT certificate and returns it to theAUT 7 MU.A through MU, B_i requests SP.B_i to verify the certificate C.SP.A.AUT of token SP.A: MU.A -> MU.B_i -> SP.B_i: verify certificate (C.SP.A.AUT)
, AUT certificate, stores the public key PuK.SP.A.AUT and sends a confirmation to MU.A
, CS_AUT public key, then: 9.1 MU.A requests the SP.A to select and verify key PuK
, AUT key, and then returns the confirma- tion: SP.A -> MU.A: conf
, CS_AUT certificate and returns it to the
, CS_AUT, stores the public key PuK.CASP.B_i.CS_AUT and sends a confirmation to MU.A: SP.A -> MU.A: conf
, A to select and verify key PuK.CASP.B_i.CS_AUT: MU.A -> SP.A: select and verify(PuK, CASP.Bi.CS_AUT)
, CS_AUT key, and then returns the con- firmation: SP.A -> MU.A: conf
, AUT certificate and returns it to the
, AUT of token SP, B_i: MU.A -> SP.A: verify certificate (C.SP.B_i.AUT)
, AUT , stores the public key PuK.SP.B_i.AUT and sends a confirmation to, OK State 2: Token SP.A has the public key C.SP.B_i.AUT of token SP.B_i
, AUT keys and sends confirmation to the MU
, A activated (selected)
, AUT keys and sends confirmation to the MU.A: SP.A -> MU.A: conf.OK State 3: SP.A and SP.B_i tokens activated their keys, which are necessary during performing cryptographic operations; moreover, the public key of the SP.A is now known by the SP, B_i and vice versa, and can be trusted by both sides
, A to generate a random number and return it together with its ID: MU.A -> SP.A: get challenge
, A and, together with its identifier SN.SP.A sends all to MU
, B_i, signs the concatenated data using its private key, encrypts it and then through MUB_i return it to, ) || textB.SP.B_i 24. MU.A sends to SP.A the request for verification of authentication tokenPrK.SP.B_i.AUT](preToken.SP.B_i)))
, B_i generated a random number and send it together with its IDB_i: get challenge
, B_i challenge and, together with its identifier SN.SP.B_i sends all to
, A, prepares preToken.SP.A, signs the concatenated data using its private key, encrypts it and then sends to MU.A, B_i || SN.SP.Bi) || textB.SP.A
, After On this basis both parties calculate the symmetric differ- ence: KA and then create session keys to ensure confidentiality and authentication of the message . It being understood that, ENC) || Kb (ENC) || Ka (MAC) || Kb (MAC) Other more general methods for generating keys to ensure the confidentiality and authentication can be found in [15]
, The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, Proc. of 17th Int. Conf. on Computer Aided Verification (CAV'05), pp.281-285, 2005.
DOI : 10.1007/11513988_27
URL : https://hal.archives-ouvertes.fr/inria-00000408
, Protocols for Authentication and Key Establishment, 2003.
DOI : 10.1007/978-3-662-09527-0
, Chen Cryptographic Protocol Security Analysis Based on Trusted Freshness, p.2012
DOI : 10.1007/978-3-642-24073-7_8
, On the security of public key protocols, 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pp.198-207, 1983.
DOI : 10.1109/SFCS.1981.32
, Certificate-Based Encryption Scheme with General Access Structure, CISIM 2012, pp.41-55
DOI : 10.1007/978-3-642-33260-9_3
, A Practical Certificate and Identity Based Encryption Scheme and Related Security Architecture, CISIM 2013, pp.178-193, 2013.
DOI : 10.1007/978-3-642-40925-7_19
URL : https://hal.archives-ouvertes.fr/hal-01496066
, Implicit and Explicit Certificates-Based Encryption Scheme, CISIM 2014, pp.651-666, 2014.
DOI : 10.1007/978-3-642-33260-9_3
URL : https://hal.archives-ouvertes.fr/hal-01405660
, Verifying Security Protocols Modeled by Networks of Automata , Fund, Inform, vol.79, issue.3-4, pp.453-471, 2007.
, Several practical protocols for authentication and key exchange, Information Processing Letters, vol.53, issue.2, pp.91-96, 1995.
DOI : 10.1016/0020-0190(94)00178-2
, Parallel Bounded Model Checking of Security Protocols, Proc. of PPAM'13, pp.224-234, 2014.
, A New Effective Approach for Modeling and Verification of Security Protocols, Proceedings of 21th international Workshop on Concurrency , Specification and Programming, pp.191-202, 2012.
, Hardware-Assisted Application-Level Access Control, ISC 2009, pp.363-378, 2009.
, Information technology ? Security techniques ? Key management ? Part 3: Mechanisms using asymmetric techniques, pp.11770-11773, 2008.