Newer
Older
4001
4002
4003
4004
4005
4006
4007
4008
4009
4010
4011
4012
4013
4014
4015
4016
4017
4018
4019
4020
4021
4022
4023
4024
4025
4026
4027
4028
4029
log("f_verify_pki_request_message: Failed to decrypt message");
return false;
}
log("f_verify_pki_request_message: v_ieee1609dot2_signed_data= ", v_ieee1609dot2_signed_data);
log("f_verify_pki_request_message: p_aes_enc_key= ", p_aes_enc_key);
// 3. Check basics security
log(
match(
v_ieee1609dot2_signed_data,
mw_etsiTs103097Data_signed(
mw_signedData(
-,
mw_toBeSignedData(
mw_signedDataPayload,
mw_ieee1609Dot2_headerInfo(c_its_aid_SCR)
)
)
)));
if (match(v_ieee1609dot2_signed_data, mw_etsiTs103097Data_signed(mw_signedData(-, mw_toBeSignedData(mw_signedDataPayload)))) == false) {
log("f_verify_pki_request_message: Failed to check basic security");
if (p_check_security == true) {
return false;
}
}
// 4. Verifiy signature
log("f_verify_pki_request_message: v_ieee1609dot2_signed_data.content.signedData.tbsData= ", v_ieee1609dot2_signed_data.content.signedData.tbsData);
v_msg := bit2oct(encvalue(v_ieee1609dot2_signed_data.content.signedData.tbsData));
log("f_verify_pki_request_message: v_msg= ", v_msg);
if (p_issuer == ''O) { // self
log("f_verify_pki_request_message: Issuer is self, check outer signature using IUT public key (PICS_ITS_S_SIGN_xxx_PUBLIC_KEY)");
var PublicVerificationKey v_verification_key;
log("f_verify_pki_request_message: PX_VE_ALG=", PX_VE_ALG);
if (PX_VE_ALG == e_nist_p256) {
if (PICS_ITS_S_SIGN_NISTP256_PUBLIC_KEY[0] == '02'O) {
v_verification_key.ecdsaNistP256.compressed_y_0 := substr(PICS_ITS_S_SIGN_NISTP256_PUBLIC_KEY, 1, 32);
} else {
v_verification_key.ecdsaNistP256.compressed_y_1 := substr(PICS_ITS_S_SIGN_NISTP256_PUBLIC_KEY, 1, 32);
}
} else if (PX_VE_ALG == e_brainpool_p256_r1) {
Yann Garcia
committed
if (PICS_ITS_S_SIGN_BRAINPOOLP256r1_PUBLIC_KEY[0] == '02'O) {
v_verification_key.ecdsaBrainpoolP256r1.compressed_y_0 := substr(PICS_ITS_S_SIGN_BRAINPOOLP256r1_PUBLIC_KEY, 1, 32);
Yann Garcia
committed
v_verification_key.ecdsaBrainpoolP256r1.compressed_y_1 := substr(PICS_ITS_S_SIGN_BRAINPOOLP256r1_PUBLIC_KEY, 1, 32);
}
} else if (PX_VE_ALG == e_brainpool_p384_r1) {
Yann Garcia
committed
if (PICS_ITS_S_SIGN_BRAINPOOLP384r1_PUBLIC_KEY[0] == '02'O) {
v_verification_key.ecdsaBrainpoolP384r1.compressed_y_0 := substr(PICS_ITS_S_SIGN_BRAINPOOLP384r1_PUBLIC_KEY, 1, 48);
Yann Garcia
committed
v_verification_key.ecdsaBrainpoolP384r1.compressed_y_1 := substr(PICS_ITS_S_SIGN_BRAINPOOLP384r1_PUBLIC_KEY, 1, 48);
}
}
log("f_verify_pki_request_message: v_verification_key=", v_verification_key);
if (f_verifyEcdsa(v_msg, int2oct(0, 32), v_ieee1609dot2_signed_data.content.signedData.signature_, v_verification_key) == false) {
if (p_check_security == true) {
return false;
}
}
//return false;
if (f_getCertificateFromDigest(f_hashedId8FromSha256(p_issuer), v_certificate, v_certificate_id) == false) {
if (p_check_security == true) {
return false;
}
}
log("f_verify_pki_request_message: v_certificate= ", v_certificate);
if (f_verifyEcdsa(v_msg, p_issuer, v_ieee1609dot2_signed_data.content.signedData.signature_, v_certificate.toBeSigned.verifyKeyIndicator.verificationKey) == false) {
if (p_check_security == true) {
return false;
}
}
}
// 4. Return the PKI message
log("f_verify_pki_request_message: v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData= ", v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData);
v_msg_bit := oct2bit(v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData);
if (decvalue(v_msg_bit, p_etsi_ts_102941_data) != 0) {
if (p_check_security == true) {
return false;
}
}
if (p_etsi_ts_102941_data.version != PkiProtocolVersion) {
if (p_check_security == true) {
return false;
}
}
log("<<< f_verify_pki_request_message: true");
return true;
} // End of function f_verify_pki_request_message
* @desc Verify the protocol element of the Pki message.
* If p_check_security is set to false, only decryption and decoding of the outer message are verified.
* @param p_private_key Private key for decryption
* @param p_publicEphemeralCompressedKey
* @param p_publicEphemeralCompressedKeyMode
* @param p_issuer Issuer
* @param p_certificate Certificate to use for verification key
* @param p_ieee1609dot2_encrypted_and_signed_data The received encrypted and signed data
* @param p_check_security Set to true to verify PKI protocol element such as signatures...
* @param p_response_type Response type (0: InnerEcResponse, 1: InnerAtResponse...). Default: 0
* @param p_etsi_ts_102941_data The EtsiTs102941Data message
* @return true on success, false otherwise
*/
function f_verify_pki_response_message(
in octetstring p_private_enc_key,
in Oct16 p_aes_sym_key,
in Oct16 p_authentication_vector, // TODO Tobe removed
in octetstring p_issuer,
in Ieee1609Dot2Data p_ieee1609dot2_encrypted_and_signed_data,
in boolean p_check_security := true,
in integer p_response_type := 0,
out EtsiTs102941Data p_etsi_ts_102941_data
) return boolean {
var octetstring v_public_enc_key;
var integer v_compressed_enc_key_mode;
var octetstring v_plain_message;
var Ieee1609Dot2Data v_ieee1609dot2_signed_data;
var bitstring v_etsi_ts_102941_data_msg;
var bitstring v_tbs;
var boolean v_ret;
log(">>> f_verify_pki_response_message: p_private_enc_key= ", p_private_enc_key);
log(">>> f_verify_pki_response_message: p_aes_sym_key= ", p_aes_sym_key);
log(">>> f_verify_pki_response_message: p_authentication_vector= ", p_authentication_vector);
log(">>> f_verify_pki_response_message: p_issuer= ", p_issuer);
log(">>> f_verify_pki_response_message: p_check_security= ", p_check_security);
log(">>> f_verify_pki_response_message: p_response_type= ", p_response_type);
// TODO Check p_ieee1609dot2_encrypted_and_signed_data.content.encryptedData.recipients[0].pskRecipInfo. See IEEE Std 1609.2-2017 Clause 6.3.34 PreSharedKeyRecipientInfo
// 1. Decrypt the data
v_plain_message := fx_decrypt_aes_128_ccm_test(p_aes_sym_key, p_ieee1609dot2_encrypted_and_signed_data.content.encryptedData.ciphertext.aes128ccm.nonce, p_ieee1609dot2_encrypted_and_signed_data.content.encryptedData.ciphertext.aes128ccm.ccmCiphertext);
if (isbound(v_plain_message) == false) {
return false;
}
log("f_verify_pki_response_message: v_plain_message= ", v_plain_message);
// 2. Decode it
v_tbs := oct2bit(v_plain_message);
if (decvalue(v_tbs, v_ieee1609dot2_signed_data) != 0) {
log("f_verify_pki_response_message: v_ieee1609dot2_signed_data= ", v_ieee1609dot2_signed_data);
log("f_verify_pki_response_message: v_ieee1609dot2_signed_data.content.signedData.tbsData= ", v_ieee1609dot2_signed_data.content.signedData.tbsData);
v_tbs := encvalue(v_ieee1609dot2_signed_data.content.signedData.tbsData);
if (f_getCertificateFromDigest(v_ieee1609dot2_signed_data.content.signedData.signer.digest, v_certificate, v_certificate_id) == false) {
if (p_check_security == true) {
return false;
}
}
if (f_verifyEcdsa(bit2oct(v_tbs), p_issuer, v_ieee1609dot2_signed_data.content.signedData.signature_, v_certificate.toBeSigned.verifyKeyIndicator.verificationKey) == false) {
if (p_check_security == true) {
return false;
}
// 4. Verify EtsiTs103097Data-Signed HeaderInfo
// TODO Parameter p_response_type seems to be useless
if ((p_response_type == 0) or (p_response_type == 1)) { // InnerEcResponse & InnerAtResponse
log("f_verify_pki_response_message: headerInfo matching= ", match(v_ieee1609dot2_signed_data.content.signedData.tbsData.headerInfo, mw_headerInfo_inner_pki_response));
if (match(v_ieee1609dot2_signed_data.content.signedData.tbsData.headerInfo, mw_headerInfo_inner_pki_response) == false) {
if (p_check_security == true) {
return false;
}
}
} // else, no check
// 5. Return the PKI message
log("f_verify_pki_response_message: v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData= ", v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData);
v_etsi_ts_102941_data_msg := oct2bit(v_ieee1609dot2_signed_data.content.signedData.tbsData.payload.data.content.unsecuredData);
if (decvalue(v_etsi_ts_102941_data_msg, p_etsi_ts_102941_data) != 0) {
return false;
}
if (p_etsi_ts_102941_data.version != PkiProtocolVersion) {
} // End of function f_verify_pki_response_message
* @desc Verify the EC certificate generated by the EA entity
* @param p_ec_certificate The new EC certificate
* @param p_ea_certificate The certificate issuer
* @param p_public_key_compressed The public compressed key (canonical form) generated for the InnerEcRequest
* @param p_compressed_mode The public compressed key mode
* @return true on success, false otherwise
*/
function f_verify_ec_certificate(
in Certificate p_ec_certificate,
in octetstring p_public_key_compressed,
in integer p_compressed_mode
) return boolean {
var HashedId8 v_ec_cert_hashed_id8;
// Calculate the HashedId8 of the whole certificate
v_encoded_cert := encvalue(p_ec_certificate);
v_ec_cert_hash := f_hashWithSha256(bit2oct(v_encoded_cert));
log("f_verify_ec_certificate: ==> EC certificate Hash: ", v_ec_cert_hash);
v_ec_cert_hashed_id8 := f_hashedId8FromSha256(v_ec_cert_hash);
log("f_verify_ec_certificate: ==> EC certificate HashedId8: ", v_ec_cert_hashed_id8);
// Check the signer
log("f_verify_ec_certificate: ", match(p_ec_certificate.issuer, mw_issuerIdentifier_sha256AndDigest));
if (match(p_ec_certificate.issuer, mw_issuerIdentifier_sha256AndDigest) == false) {
log("f_verify_ec_certificate: Wrong issuer");
if (f_verifyCertificateSignatureWithPublicKey(p_ec_certificate, p_ea_certificate.toBeSigned.verifyKeyIndicator.verificationKey) == false) {
log("f_verify_ec_certificate: Signature not verified");
return false;
// TODO Check that requested information are present
if (f_verifySspPermissions(p_ec_certificate.toBeSigned.appPermissions, p_ea_certificate.toBeSigned.appPermissions) == false) {
log("f_verify_ec_certificate: Ssp permissions not verified");
return false;
}
return true;
} // End of function f_verify_ec_certificate
* @desc Verify the generated AT certificate
* @param p_at_certificate The new AT certificate
* @param p_ea_certificate The certificate issuer
* @param p_public_key_compressed The public compressed key (canonical form) generated for the InnerAtRequest
* @param p_compressed_mode The public compressed key mode
* @return true on success, false otherwise
*/
function f_verify_at_certificate(
in Certificate p_at_certificate,
in Certificate p_aa_certificate,
in octetstring p_public_key_compressed,
in integer p_compressed_mode
) return boolean {
var bitstring v_encoded_cert;
var HashedId8 v_at_cert_hashed_id8;
// Calculate the HashedId8 of the whole certificate
v_encoded_cert := encvalue(p_at_certificate);
v_at_cert_hashed_id8 := f_hashedId8FromSha256(f_hashWithSha256(bit2oct(v_encoded_cert)));
log("f_verify_at_certificate: EC certificate HashedId8: ", v_at_cert_hashed_id8);
// Check the signer
log("f_verify_at_certificate: ", match(p_at_certificate.issuer, mw_issuerIdentifier_self()));
if (match(p_at_certificate.issuer, mw_issuerIdentifier_self)) {
return false;
}
// Check EC certificate signature
if (f_verifyCertificateSignatureWithPublicKey(p_at_certificate, p_aa_certificate.toBeSigned.verifyKeyIndicator.verificationKey) == false) {
log("f_verify_at_certificate: Signature not verified");
return false;
}
// TODO Check that requested information are present
if (f_verifySspPermissions(p_aa_certificate.toBeSigned.appPermissions, p_at_certificate.toBeSigned.appPermissions) == false) {
log("f_verify_ec_certificate: Ssp permissions not verified");
return false;
}
return true;
} // End of function f_verify_at_certificate
group security_function { // TODO To be moved in LibItsSecurity_Function module
function f_extract_enc_key(
in Certificate p_certificate,
out octetstring p_public_enc_key,
out integer p_compressed_enc_key_mode
) return boolean {
log(">>> f_extract_enc_key: ", p_certificate);
if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesNistP256)) {
if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesNistP256.compressed_y_0)) {
p_public_enc_key := p_certificate.toBeSigned.encryptionKey.publicKey.eciesNistP256.compressed_y_0;
p_compressed_enc_key_mode := 0;
} else if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesNistP256.compressed_y_1)) {
p_public_enc_key := p_certificate.toBeSigned.encryptionKey.publicKey.eciesNistP256.compressed_y_1;
p_compressed_enc_key_mode := 1;
log("f_extract_enc_key: Non canonical certificate: ", p_certificate);
return false;
}
} else if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesBrainpoolP256r1)) {
if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesBrainpoolP256r1.compressed_y_0)) {
p_public_enc_key := p_certificate.toBeSigned.encryptionKey.publicKey.eciesBrainpoolP256r1.compressed_y_0;
p_compressed_enc_key_mode := 0;
} else if (ischosen(p_certificate.toBeSigned.encryptionKey.publicKey.eciesBrainpoolP256r1.compressed_y_1)) {
p_public_enc_key := p_certificate.toBeSigned.encryptionKey.publicKey.eciesBrainpoolP256r1.compressed_y_1;
p_compressed_enc_key_mode := 0;
} else {
log("f_extract_enc_key: Non canonical certificate: ", p_certificate);
log("f_extract_enc_key: Invalid certificate: ", p_certificate);
return false;
}
return true;
} // End of function f_extract_enc_key
} // End of group security_function
altstep a_default_pki_http() runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(mw_http_request) {
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
} // End of altstep a_default_pki_http
altstep a_default_pki_http_ec() runs on ItsPkiHttp {
[PICS_MULTIPLE_END_POINT] httpEcPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[PICS_MULTIPLE_END_POINT] httpEcPort.receive(mw_http_request) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpEcPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
4388
4389
4390
4391
4392
4393
4394
4395
4396
4397
4398
4399
4400
4401
4402
4403
4404
4405
4406
4407
4408
4409
4410
4411
4412
4413
4414
} // End of altstep a_default_pki_http_ec
altstep a_default_pki_http_atv() runs on ItsPkiHttp {
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive(mw_http_request) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
4419
4420
4421
4422
4423
4424
4425
4426
4427
4428
4429
4430
4431
4432
4433
4434
4435
4436
4437
4438
4439
4440
4441
4442
4443
4444
4445
} // End of altstep a_default_pki_http_atv
altstep a_default_pki_http_at() runs on ItsPkiHttp {
[PICS_MULTIPLE_END_POINT] httpAtPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtPort.receive(mw_http_request) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpAtPort.receive {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
4452
4453
4454
4455
4456
4457
4458
4459
4460
4461
4462
4463
4464
4465
4466
4467
4468
4469
4470
4471
4472
4473
4474
4475
4476
4477
4478
4479
4480
4481
4482
altstep a_default_pki_http_ca() runs on ItsPkiHttp {
[PICS_MULTIPLE_END_POINT] httpCaPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[PICS_MULTIPLE_END_POINT] httpCaPort.receive(mw_http_request) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpCaPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpCaPort.receive {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
} // End of altstep a_default_pki_http_ca
4483
4484
4485
4486
4487
4488
4489
4490
4491
4492
4493
4494
4495
4496
4497
4498
4499
4500
4501
4502
4503
4504
4505
4506
4507
4508
4509
4510
4511
4512
4513
altstep a_default_pki_http_tlm() runs on ItsPkiHttp {
[PICS_MULTIPLE_END_POINT] httpTlmPort.receive(
mw_http_response(
mw_http_response_ko
)) {
tc_ac.stop;
log("*** " & testcasename() & ": FAIL: Unexpected message received ***");
f_selfOrClientSyncAndVerdictTestBody(c_tbDone, e_error);
}
[PICS_MULTIPLE_END_POINT] httpTlmPort.receive(mw_http_request) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Request received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpTlmPort.receive(mw_http_response) {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP Response received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[PICS_MULTIPLE_END_POINT] httpTlmPort.receive {
tc_ac.stop;
log("*** a_default: ERROR: Unexpected HTTP message received ***");
f_selfOrClientSyncAndVerdict("error", e_error);
}
[] a_shutdown() {
log("*** a_default: INFO: TEST COMPONENT NOW STOPPING ITSELF! ***");
stop;
}
} // End of altstep a_default_pki_http_tlm
altstep a_await_ec_http_request_from_iut(
template HttpMessage p_http_message,
out HttpMessage p_response
) runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(p_http_message) -> value p_response {
log("a_await_ec_http_request_from_iut: Received message on httpPort");
}
[PICS_MULTIPLE_END_POINT] httpEcPort.receive(p_http_message) -> value p_response {
log("a_await_ec_http_request_from_iut: Received message on httpEcPort");
}
} // End of altstep a_await_ec_http_request_from_iut
4526
4527
4528
4529
4530
4531
4532
4533
4534
4535
4536
4537
4538
4539
4540
4541
4542
4543
4544
4545
4546
4547
4548
4549
altstep a_await_ec_http_response_from_iut(
template HttpMessage p_http_message,
out HttpMessage p_response
) runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(p_http_message) -> value p_response {
log("a_await_ec_http_response_from_iut: Received message on httpPort");
}
[PICS_MULTIPLE_END_POINT] httpEcPort.receive(p_http_message) -> value p_response {
log("a_await_ec_http_response_from_iut: Received message on httpEcPort");
}
} // End of altstep a_await_ec_http_response_from_iut
altstep a_await_at_http_response_from_iut(
template HttpMessage p_http_message,
out HttpMessage p_response
) runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(p_http_message) -> value p_response {
log("a_await_at_http_response_from_iut: Received message on httpPort");
}
[PICS_MULTIPLE_END_POINT] httpAtPort.receive(p_http_message) -> value p_response {
log("a_await_at_http_response_from_iut: Received message on httpAtPort");
}
} // End of altstep a_await_at_http_response_from_iut
altstep a_await_atv_http_request_from_iut(
template HttpMessage p_http_message,
out HttpMessage p_request
) runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(p_http_message) -> value p_request {
log("a_await_atv_http_request_from_iut: Received message on httpPort");
}
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive(p_http_message) -> value p_request {
log("a_await_avt_http_request_from_iut: Received message on httpAtVPort");
}
} // End of altstep a_await_atv_http_request_from_iut
template HttpMessage p_http_message,
out HttpMessage p_response
) runs on ItsPkiHttp {
[not(PICS_MULTIPLE_END_POINT)] httpPort.receive(p_http_message) -> value p_response {
log("a_await_atv_http_response_from_iut: Received message on httpPort");
}
[PICS_MULTIPLE_END_POINT] httpAtVPort.receive(p_http_message) -> value p_response {
log("a_await_avt_http_response_from_iut: Received message on httpAtVPort");
}
} // End of altstep a_await_atv_http_response_from_iut