On the Verification of Data Encryption Requirements in Internet of Things Using Event-B

Imed Abbassi; Layth Sliman; Mohamed Graiet; Walid Gaaloul

doi:10.1007/978-3-030-30874-2_11

On the Verification of Data Encryption Requirements in Internet of Things Using Event-B

Imed Abbassi
, Layth Sliman
, Mohamed Graiet
, Walid Gaaloul

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

In this paper, an approach for verifying data exchange requirements in the context of IoT with regard to resource constraints is described. The verification is done using Event-B method. The security requirements are defined based on the correlation concept. The capacity requirements are defined as a set of constraints on the exchanged data. The proposed approach starts by formalizing the data exchange process. Second, it extends this formalization with the data exchange security and capacity requirements. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we use ProB model-checker to trace possible design errors.

Original language	English
Title of host publication	Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings
Editors	Rim Jallouli, Mohamed Anis Bach Tobji, Deny Bélisle, Sehl Mellouli, Farid Abdallah, Ibrahim Osman
Publisher	Springer
Pages	147-156
Number of pages	10
ISBN (Print)	9783030308735
DOIs	https://doi.org/10.1007/978-3-030-30874-2_11
Publication status	Published - 1 Jan 2019
Event	4th International Conference on Digital Economy, ICDEc 2019 - Beirut, Lebanon Duration: 15 Apr 2019 → 18 Apr 2019

Publication series

Name	Lecture Notes in Business Information Processing
Volume	358
ISSN (Print)	1865-1348
ISSN (Electronic)	1865-1356

Conference

Conference	4th International Conference on Digital Economy, ICDEc 2019
Country/Territory	Lebanon
City	Beirut
Period	15/04/19 → 18/04/19

Access to Document

10.1007/978-3-030-30874-2_11

Cite this

Abbassi, I., Sliman, L., Graiet, M., & Gaaloul, W. (2019). On the Verification of Data Encryption Requirements in Internet of Things Using Event-B. In R. Jallouli, M. A. Bach Tobji, D. Bélisle, S. Mellouli, F. Abdallah, & I. Osman (Eds.), Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings (pp. 147-156). (Lecture Notes in Business Information Processing; Vol. 358). Springer. https://doi.org/10.1007/978-3-030-30874-2_11

Abbassi, Imed ; Sliman, Layth ; Graiet, Mohamed et al. / On the Verification of Data Encryption Requirements in Internet of Things Using Event-B. Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings. editor / Rim Jallouli ; Mohamed Anis Bach Tobji ; Deny Bélisle ; Sehl Mellouli ; Farid Abdallah ; Ibrahim Osman. Springer, 2019. pp. 147-156 (Lecture Notes in Business Information Processing).

@inproceedings{776a3273c7e94ec68d63e7c3a7e652e0,

title = "On the Verification of Data Encryption Requirements in Internet of Things Using Event-B",

abstract = "In this paper, an approach for verifying data exchange requirements in the context of IoT with regard to resource constraints is described. The verification is done using Event-B method. The security requirements are defined based on the correlation concept. The capacity requirements are defined as a set of constraints on the exchanged data. The proposed approach starts by formalizing the data exchange process. Second, it extends this formalization with the data exchange security and capacity requirements. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we use ProB model-checker to trace possible design errors.",

author = "Imed Abbassi and Layth Sliman and Mohamed Graiet and Walid Gaaloul",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 4th International Conference on Digital Economy, ICDEc 2019 ; Conference date: 15-04-2019 Through 18-04-2019",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-30874-2\_11",

language = "English",

isbn = "9783030308735",

series = "Lecture Notes in Business Information Processing",

publisher = "Springer",

pages = "147--156",

editor = "Rim Jallouli and \{Bach Tobji\}, \{Mohamed Anis\} and Deny B{\'e}lisle and Sehl Mellouli and Farid Abdallah and Ibrahim Osman",

booktitle = "Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings",

}

Abbassi, I, Sliman, L, Graiet, M & Gaaloul, W 2019, On the Verification of Data Encryption Requirements in Internet of Things Using Event-B. in R Jallouli, MA Bach Tobji, D Bélisle, S Mellouli, F Abdallah & I Osman (eds), Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings. Lecture Notes in Business Information Processing, vol. 358, Springer, pp. 147-156, 4th International Conference on Digital Economy, ICDEc 2019, Beirut, Lebanon, 15/04/19. https://doi.org/10.1007/978-3-030-30874-2_11

On the Verification of Data Encryption Requirements in Internet of Things Using Event-B. / Abbassi, Imed; Sliman, Layth; Graiet, Mohamed et al.
Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings. ed. / Rim Jallouli; Mohamed Anis Bach Tobji; Deny Bélisle; Sehl Mellouli; Farid Abdallah; Ibrahim Osman. Springer, 2019. p. 147-156 (Lecture Notes in Business Information Processing; Vol. 358).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - On the Verification of Data Encryption Requirements in Internet of Things Using Event-B

AU - Abbassi, Imed

AU - Sliman, Layth

AU - Graiet, Mohamed

AU - Gaaloul, Walid

PY - 2019/1/1

Y1 - 2019/1/1

N2 - In this paper, an approach for verifying data exchange requirements in the context of IoT with regard to resource constraints is described. The verification is done using Event-B method. The security requirements are defined based on the correlation concept. The capacity requirements are defined as a set of constraints on the exchanged data. The proposed approach starts by formalizing the data exchange process. Second, it extends this formalization with the data exchange security and capacity requirements. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we use ProB model-checker to trace possible design errors.

AB - In this paper, an approach for verifying data exchange requirements in the context of IoT with regard to resource constraints is described. The verification is done using Event-B method. The security requirements are defined based on the correlation concept. The capacity requirements are defined as a set of constraints on the exchanged data. The proposed approach starts by formalizing the data exchange process. Second, it extends this formalization with the data exchange security and capacity requirements. The consistency of each model and the relationship between an abstract model and its refinements are obtained by formal proofs. Finally, we use ProB model-checker to trace possible design errors.

U2 - 10.1007/978-3-030-30874-2_11

DO - 10.1007/978-3-030-30874-2_11

M3 - Conference contribution

AN - SCOPUS:85076102595

SN - 9783030308735

T3 - Lecture Notes in Business Information Processing

SP - 147

EP - 156

BT - Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings

A2 - Jallouli, Rim

A2 - Bach Tobji, Mohamed Anis

A2 - Bélisle, Deny

A2 - Mellouli, Sehl

A2 - Abdallah, Farid

A2 - Osman, Ibrahim

PB - Springer

T2 - 4th International Conference on Digital Economy, ICDEc 2019

Y2 - 15 April 2019 through 18 April 2019

ER -

Abbassi I, Sliman L, Graiet M, Gaaloul W. On the Verification of Data Encryption Requirements in Internet of Things Using Event-B. In Jallouli R, Bach Tobji MA, Bélisle D, Mellouli S, Abdallah F, Osman I, editors, Digital Economy. Emerging Technologies and Business Innovation - 4th International Conference, ICDEc 2019, Proceedings. Springer. 2019. p. 147-156. (Lecture Notes in Business Information Processing). doi: 10.1007/978-3-030-30874-2_11

On the Verification of Data Encryption Requirements in Internet of Things Using Event-B

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this