Kammueller, F.; Kirsal-Ever, Y.; Cheng, X.

DNSsec in Isabelle – replay attack and origin authentication

Conference paper

Kammueller, F., Kirsal-Ever, Y. and Cheng, X. 2013. DNSsec in Isabelle – replay attack and origin authentication. SMC 2013: IEEE International Conference on Systems, Man, and Cybernetics. Manchester, UK 13 - 16 Oct 2013 IEEE. pp. 4772-4777 https://doi.org/10.1109/SMC.2013.812

ISBN
Type	Conference paper
Title	DNSsec in Isabelle – replay attack and origin authentication
Authors	Kammueller, F., Kirsal-Ever, Y. and Cheng, X.
Abstract	In this paper, we present a formal model and analysis for the security extensions of the Domain Name System (DNSsec) in the interactive theorem prover Isabelle/HOL. Based on the inductive approach of security protocol analysis by Paulson in Isabelle/HOL, we show how the protocol can be modelled and important properties are proved. We prove that origin authentication works securely. In order to illustrate that the model is adequate, we show gthat previous domain name requests can be replayed -- as in the classical DNS -- by an attacker. These replays luckily can be uniquely identified in DNSsec due to the origin authentication mechanism that we establish to enhance security.
Keywords	DNSsec; Isabelle/HOL; authentication; replay attack
Conference	SMC 2013: IEEE International Conference on Systems, Man, and Cybernetics
Page range	4772-4777
Proceedings Title	2013 IEEE International Conference on Systems, Man, and Cybernetics
Series	IEEE International Conference on Systems Man and Cybernetics Conference Proceedings
ISSN	1062-922X
Electronic	9781479906529
Publisher	IEEE
Publication dates
Print	13 Oct 2013
Print	27 Jan 2014
Publication process dates
Deposited	23 Apr 2015
Output status	Published
Digital Object Identifier (DOI)	https://doi.org/10.1109/SMC.2013.812
Web of Science identifier	WOS:000332201904155
Web address (URL) of conference proceedings	https://ieeexplore.ieee.org/xpl/conhome/6689802/proceeding
Language	English

Permalink -

https://repository.mdx.ac.uk/item/85157

Log in to edit

108
total views
0
total downloads
12
views this month
0
downloads this month

Export as

Related outputs

Formalizing federated learning and differential privacy for GIS systems in IIIf

Kammueller, F., Piras, L., Fields, B. and Nagarajan, R. 2024. Formalizing federated learning and differential privacy for GIS systems in IIIf. 3rd International Workshop on System Security Assurance. Bydgoszcz, Poland 19 - 20 Sep 2024 Springer.

Transparency vs explanation of machine learning algorithms: perspectives from recent legal proceedings

Nnawuchi, U., George, C. and Kammueller, F. 2024. Transparency vs explanation of machine learning algorithms: perspectives from recent legal proceedings. Santos M., Machado, J., Novais, P., Cortez, P. and Moreira, P. (ed.) 23rd International Conference on Artificial Intelligence. Viana do Castelo, Portugal 03 - 06 Sep 2024 Springer. pp. 270-283 https://doi.org/10.1007/978-3-031-73497-7_22

Analyzing air-traffic security using GIS-``blur'' with information flow control in the IIIf

Kammueller, F. 2024. Analyzing air-traffic security using GIS-``blur'' with information flow control in the IIIf. 19th International Conference on Availability, Reliability and Security. Vienna, Austria 30 Jul - 02 Aug 2024 New York, NY Association for Computing Machinery (ACM). pp. 68 https://doi.org/10.1145/3664476

Introducing distributed ledger security into system specifications with the Isabelle RR-cycle

Kammueller, F. 2024. Introducing distributed ledger security into system specifications with the Isabelle RR-cycle. 28th European Symposium on Research in Computer Security: 2nd International Workshop on System Security Assurance (SecAssure). The Hague, The Netherlands 29 - 29 Sep 2023 Springer. pp. 330-340 https://doi.org/10.1007/978-3-031-54129-2_19

Social and moral psychology of COVID-19 across 69 countries

Azevedo, F., Pavlović, T., Rêgo, G., Ay, F., Gjoneska, B., Etienne, T., Ross, R., Schönegger, P., Riaño-Moreno, J., Cichocka, A., Capraro, V., Cian, L., Longoni, C., Chan, H., Van Bavel, J., Sjåstad, H., Nezlek, J., Alfano, M., Gelfand, M., Birtel, M., Cislak, A., Lockwood, P., Abts, K., Agadullina, E., Aruta, J., Besharati, S., Bor, A., Choma, B., Crabtree, C., Cunningham, W., De, K., Ejaz, W., Elbaek, C., Findor, A., Flichtentrei, D., Franc, R., Gruber, J., Gualda, E., Horiuchi, Y., Huynh, T., Ibanez, A., Imran, M., Israelashvili, J., Jasko, K., Kantorowicz, J., Kantorowicz-Reznichenko, E., Krouwel, A., Laakasuo, M., Lamm, C., Leygue, C., Lin, M., Mansoor, M., Marie, A., Mayiwar, L., Mazepus, H., McHugh, C., Minda, J., Mitkidis, P., Olsson, A., Otterbring, T., Packer, D., Perry, A., Petersen, M., Puthillam, A., Rothmund, T., Santamaría-García, H., Schmid, P., Stoyanov, D., Tewari, S., Todosijević, B., Tsakiris, M., Tung, H., Umbres, R., Vanags, E., Vlasceanu, M., Vonasch, A., Yucel, M., Zhang, Y., Abad, M., Adler, E., Akrawi, N., Mdarhri, H., Amara, H., Amodio, D., Antazo, B., Apps, M., Ba, M., Barbosa, S., Bastian, B., Berg, A., Bernal-Zárate, M., Bernstein, M., Białek, M., Bilancini, E., Bogatyreva, N., Boncinelli, L., Booth, J., Borau, S., Buchel, O., Cameron, C., Carvalho, C., Celadin, T., Cerami, C., Chalise, H., Cheng, X., Cockcroft, K., Conway, J., Córdoba-Delgado, M., Crespi, C., Crouzevialle, M., Cutler, J., Cypryańska, M., Dabrowska, J., Daniels, M., Davis, V., Dayley, P., Delouvée, S., Denkovski, O., Dezecache, G., Dhaliwal, N., Diato, A., Di Paolo, R., Drosinou, M., Dulleck, U., Ekmanis, J., Ertan, A., Farhana, H., Farkhari, F., Farmer, H., Fenwick, A., Fidanovski, K., Flew, T., Fraser, S., Frempong, R., Fugelsang, J., Gale, J., Garcia-Navarro, E., Garladinne, P., Ghajjou, O., Gkinopoulos, T., Gray, K., Griffin, S., Gronfeldt, B., Gümren, M., Gurung, R., Halperin, E., Harris, E., Herzon, V., Hruška, M., Huang, G., Hudecek, M., Isler, O., Jangard, S., Jorgensen, F., Kachanoff, F., Kahn, J., Dangol, A., Keudel, O., Koppel, L., Koverola, M., Kubin, E., Kunnari, A., Kutiyski, Y., Laguna, O., Leota, J., Lermer, E., Levy, J., Levy, N., Li, C., Long, E., Maglić, M., McCashin, D., Metcalf, A., Mikloušić, I., El Mimouni, S., Miura, A., Molina-Paredes, J., Monroy-Fonseca, C., Morales-Marente, E., Moreau, D., Muda, R., Myer, A., Nash, K., Nesh-Nash, T., Nitschke, J., Nurse, M., Ohtsubo, Y., de Mello, V., O’Madagain, C., Onderco, M., Palacios-Galvez, M., Palomöki, J., Pan, Y., Papp, Z., Pärnamets, P., Paruzel-Czachura, M., Pavlović, Z., Payán-Gómez, C., Perander, S., Pitman, M., Prasad, R., Pyrkosz-Pacyna, J., Rathje, S., Raza, A., Rhee, K., Robertson, C., Rodríguez-Pascual, I., Saikkonen, T., Salvador-Ginez, O., Santi, G., Santiago-Tovar, N., Savage, D., Scheffer, J., Schultner, D., Schutte, E., Scott, A., Sharma, M., Sharma, P., Skali, A., Stadelmann, D., Stafford, C., Stanojević, D., Stefaniak, A., Sternisko, A., Stoica, A., Stoyanova, K., Strickland, B., Sundvall, J., Thomas, J., Tinghög, G., Torgler, B., Traast, I., Tucciarelli, R., Tyrala, M., Ungson, N., Uysal, M., Van Lange, P., van Prooijen, J., van Rooy, D., Västfjäll, D., Verkoeijen, P., Vieira, J., von Sikorski, C., Walker, A., Watermeyer, J., Wetter, E., Whillans, A., White, K., Habib, R., Willardt, R., Wohl, M., Wójcik, A., Wu, K., Yamada, Y., Yilmaz, O., Yogeeswaran, K., Ziemer, C., Zwaan, R., Boggio, P. and Sampaio, W. 2023. Social and moral psychology of COVID-19 across 69 countries. Scientific Data. 10 (1), p. 272. https://doi.org/10.1038/s41597-023-02080-8

IHWC: intelligent hidden web crawler for harvesting data in urban domains

Kaur, S., Singh, A., Geetha, G. and Cheng, X. 2021. IHWC: intelligent hidden web crawler for harvesting data in urban domains. Complex & Intelligent Systems. https://doi.org/10.1007/s40747-022-00839-x

A tamper-resistant broadcasting scheme for secure communication in internet of autonomous vehicles

Sun, J., Tao, J., Zhang, H., Zhao, Y., Nie, L., Cheng, X. and Zhang, T. 2023. A tamper-resistant broadcasting scheme for secure communication in internet of autonomous vehicles. IEEE Transactions on Intelligent Transportation Systems. 25 (3), pp. 2837-2846. https://doi.org/10.1109/TITS.2023.3265403

Privacy-preserving and fine-grained data sharing for resource-constrained healthcare CPS devices

Bao, Y., Qiu, W. and Cheng, X. 2023. Privacy-preserving and fine-grained data sharing for resource-constrained healthcare CPS devices. Expert Systems. 40 (6). https://doi.org/10.1111/exsy.13220

A novel framework for melanoma lesion segmentation using multiparallel depthwise separable and dilated convolutions with swish activations

Bukhari, M., Yasmin, S., Habib, A., Cheng, X., Ullah, F., Yoo, J. and Lee, D. 2023. A novel framework for melanoma lesion segmentation using multiparallel depthwise separable and dilated convolutions with swish activations. Journal of Healthcare Engineering. 2023 (1). https://doi.org/10.1155/2023/1847115

Fake news stance detection using selective features and FakeNET

Aljrees, T., Cheng, X., Ahmed, M., Umer, M., Majeed, R., Alnowaiser, K., Abuzinadah, N. and Ashraf, I. 2023. Fake news stance detection using selective features and FakeNET. PLoS ONE. 18 (7). https://doi.org/10.1371/journal.pone.0287298

PIGNUS: a deep learning model for IDS in industrial internet-of-things

Jayalaxmi, P., Saha, R., Kumar, G., Alazab, M., Conti, M. and Cheng, X. 2023. PIGNUS: a deep learning model for IDS in industrial internet-of-things. Computers and Security. 132. https://doi.org/10.1016/j.cose.2023.103315

Explanation of student attendance AI prediction with the Isabelle Infrastructure Framework

Kammueller, F. and Satija, D. 2023. Explanation of student attendance AI prediction with the Isabelle Infrastructure Framework. Information. 14 (8). https://doi.org/10.3390/info14080453

Generative recorrupted-to-recorrupted: an unsupervised image denoising network for arbitrary noise distribution

Liu, Y., Wan, B., Shi, D. and Cheng, X. 2023. Generative recorrupted-to-recorrupted: an unsupervised image denoising network for arbitrary noise distribution. Remote Sensing. 15 (2). https://doi.org/10.3390/rs15020364

Cooperative conflict detection and resolution and safety assessment for 6G enabled unmanned aerial vehicles

Li, S., Cheng, X., Huang, X., Otaibi, S. and Wang, H. 2023. Cooperative conflict detection and resolution and safety assessment for 6G enabled unmanned aerial vehicles. IEEE Transactions on Intelligent Transportation Systems. 24 (2), pp. 2183-2198. https://doi.org/10.1109/TITS.2021.3137458

An efficient quality of services based wireless sensor network for anomaly detection using soft computing approaches

Mittal, M., Kobielnik, M., Gupta, S., Cheng, X. and Wozniak, M. 2022. An efficient quality of services based wireless sensor network for anomaly detection using soft computing approaches. Journal of Cloud Computing. 11 (1), pp. 1-21. https://doi.org/10.1186/s13677-022-00344-z

Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders

Kammueller, F. and Alvarado, C. 2022. Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders. Moallem, A. (ed.) HCI-CPT: 4th International Conference on HCI for Cybersecurity, Privacy and Trust. Virtual 26 Jun - 01 Jul 2022 Springer. pp. 340-357 https://doi.org/10.1007/978-3-031-05563-8_22

Explanation by automated reasoning using the Isabelle Infrastructure framework

Kammueller, F. 2021. Explanation by automated reasoning using the Isabelle Infrastructure framework. arxiv.org. https://doi.org/10.48550/arXiv.2112.14809

Efficient, revocable, and privacy-preserving fine-grained data sharing with keyword search for the cloud-assisted medical IoT system

Bao, Y., Qiu, W., Tang, P. and Cheng, X. 2022. Efficient, revocable, and privacy-preserving fine-grained data sharing with keyword search for the cloud-assisted medical IoT system. IEEE Journal of Biomedical and Health Informatics. 26 (5), pp. 2041-2051. https://doi.org/10.1109/JBHI.2021.3100871

Large-size data distribution in IoV based on 5G/6G compatible heterogeneous network

Yin, X., Liu, J., Cheng, X. and Xiong, X. 2022. Large-size data distribution in IoV based on 5G/6G compatible heterogeneous network. IEEE Transactions on Intelligent Transportation Systems. 25 (7), pp. 9840-9852. https://doi.org/10.1109/TITS.2021.3118701

A differentiated learning environment in domain model for learning disabled learners

Thapliyal, M., Ahuja, N., Shankar, A., Cheng, X. and Kumar, M. 2022. A differentiated learning environment in domain model for learning disabled learners. Journal of Computing in Higher Education. 34, pp. 60-82. https://doi.org/10.1007/s12528-021-09278-y

Offline signature verification using deep neural network with application to computer vision

Sharma, N., Gupta, S., Mehta, P., Cheng, X., Shankar, A., Singh, P. and Nayak, S. 2022. Offline signature verification using deep neural network with application to computer vision. Journal of Electronic Imaging (JEI). 31 (4). https://doi.org/10.1117/1.JEI.31.4.041210

Intrusion detection and prevention system for an IoT environment

Kumar, A., Abhishek, K., Ghalib, M., Shankar, A. and Cheng, X. 2022. Intrusion detection and prevention system for an IoT environment. Digital Communications and Networks. 8 (4), pp. 540-551. https://doi.org/10.1016/j.dcan.2022.05.027

An empirical study on Retinex methods for low-light image enhancement

Rasheed, M., Guo, G., Shi, D., Khan, H. and Cheng, X. 2022. An empirical study on Retinex methods for low-light image enhancement. Remote Sensing. 14 (18). https://doi.org/10.3390/rs14184608

A tagging SNP set method based on network community partition of linkage disequilibrium and node centrality

Wan, Q., Cheng, X., Zhang, Y., Lu, G., Wang, S. and He, S. 2022. A tagging SNP set method based on network community partition of linkage disequilibrium and node centrality. Current Bioinformatics. 17 (9), pp. 825-834. https://doi.org/10.2174/1574893617666220324155813

Explanation of black box AI for GDPR related privacy using Isabelle

Kammueller, F. 2022. Explanation of black box AI for GDPR related privacy using Isabelle. Garcia-Alfaro, J., Navarro-Arribas, G. and Dragoni, N. (ed.) 17th DPM International Workshop on Data Privacy Management. Copenhagen, Denmark 29 - 30 Sep 2022 Cham Springer. https://doi.org/10.1007/978-3-031-25734-6_5

Cyber-threat detection system using a hybrid approach of transfer learning and multi-model image representation

Ullah, F., Ullah, S., Naeem, M., Mostarda, L., Rho, S. and Cheng, X. 2022. Cyber-threat detection system using a hybrid approach of transfer learning and multi-model image representation. Sensors. 22 (15), pp. 1-26. https://doi.org/10.3390/s22155883

A deep convolutional neural network stacked ensemble for malware threat classification in internet of things

Naeem, H., Cheng, X., Ullah, F., Jabbar, S. and Dong, S. 2022. A deep convolutional neural network stacked ensemble for malware threat classification in internet of things. Journal of Circuits, Systems and Computers. 31 (17). https://doi.org/10.1142/s0218126622503029

RFAP: a revocable fine-grained access control mechanism for autonomous vehicle platoon

Zhao, Y., Wang, Y., Cheng, X., Chen, H., Yu, H. and Ren, Y. 2022. RFAP: a revocable fine-grained access control mechanism for autonomous vehicle platoon. IEEE Transactions on Intelligent Transportation Systems. 23 (7), pp. 9668-9679. https://doi.org/10.1109/TITS.2021.3105458

Predicting attitudinal and behavioral responses to COVID-19 pandemic using machine learning

Pavlović, T., Azevedo, F., De, K., Riaño-Moreno, J., Maglić, M., Gkinopoulos, T., Donnelly-Kehoe, P., Payán-Gómez, C., Huang, G., Kantorowicz, J., Birtel, M., Schönegger, P., Capraro, V., Santamaría-García, H., Yucel, M., Ibanez, A., Rathje, S., Wetter, E., Stanojević, D., van Prooijen, J., Hesse, E., Elbaek, C., Franc, R., Pavlović, Z., Mitkidis, P., Cichocka, A., Gelfand, M., Alfano, M., Ross, R., Sjåstad, H., Nezlek, J., Cislak, A., Lockwood, P., Abts, K., Agadullina, E., Amodio, D., Apps, M., Aruta, J., Besharati, S., Bor, A., Choma, B., Cunningham, W., Ejaz, W., Farmer, H., Findor, A., Gjoneska, B., Gualda, E., Huynh, T., Imran, M., Israelashvili, J., Kantorowicz-Reznichenko, E., Krouwel, A., Kutiyski, Y., Laakasuo, M., Lamm, C., Levy, J., Leygue, C., Lin, M., Mansoor, M., Marie, A., Mayiwar, L., Mazepus, H., McHugh, C., Olsson, A., Otterbring, T., Packer, D., Palomäki, J., Perry, A., Petersen, M., Puthillam, A., Rothmund, T., Schmid, P., Stadelmann, D., Stoica, A., Stoyanov, D., Stoyanova, K., Tewari, S., Todosijević, B., Torgler, B., Tsakiris, M., Tung, H., Umbreș, R., Vanags, E., Vlasceanu, M., Vonasch, A., Zhang, Y., Abad, M., Adler, E., Mdarhri, H., Antazo, B., Ay, F., Ba, M., Barbosa, S., Bastian, B., Berg, A., Białek, M., Bilancini, E., Bogatyreva, N., Boncinelli, L., Booth, J., Borau, S., Buchel, O., de Carvalho, C., Celadin, T., Cerami, C., Chalise, H., Cheng, X., Cian, L., Cockcroft, K., Conway, J., Córdoba-Delgado, M., Crespi, C., Crouzevialle, M., Cutler, J., Cypryańska, M., Dabrowska, J., Davis, V., Minda, J., Dayley, P., Delouvée, S., Denkovski, O., Dezecache, G., Dhaliwal, N., Diato, A., Di Paolo, R., Dulleck, U., Ekmanis, J., Etienne, T., Farhana, H., Farkhari, F., Fidanovski, K., Flew, T., Fraser, S., Frempong, R., Fugelsang, J., Gale, J., García-Navarro, E., Garladinne, P., Gray, K., Griffin, S., Gronfeldt, B., Gruber, J., Halperin, E., Herzon, V., Hruška, M., Hudecek, M., Isler, O., Jangard, S., Jørgensen, F., Keudel, O., Koppel, L., Koverola, M., Kunnari, A., Leota, J., Lermer, E., Li, C., Longoni, C., McCashin, D., Mikloušić, I., Molina-Paredes, J., Monroy-Fonseca, C., Morales-Marente, E., Moreau, D., Muda, R., Myer, A., Nash, K., Nitschke, J., Nurse, M., de Mello, V., Palacios-Galvez, M., Pan, Y., Papp, Z., Pärnamets, P., Paruzel-Czachura, M., Perander, S., Pitman, M., Raza, A., Rêgo, G., Robertson, C., Rodríguez-Pascual, I., Saikkonen, T., Salvador-Ginez, O., Sampaio, W., Santi, G., Schultner, D., Schutte, E., Scott, A., Skali, A., Stefaniak, A., Sternisko, A., Strickland, B., Thomas, J., Tinghög, G., Traast, I., Tucciarelli, R., Tyrala, M., Ungson, N., Uysal, M., Van Rooy, D., Västfjäll, D., Vieira, J., von Sikorski, C., Walker, A., Watermeyer, J., Willardt, R., Wohl, M., Wójcik, A., Wu, K., Yamada, Y., Yilmaz, O., Yogeeswaran, K., Ziemer, C., Zwaan, R., Boggio, P., Whillans, A., Van Lange, P., Prasad, R., Onderco, M., O'Madagain, C., Nesh-Nash, T., Laguna, O., Kubin, E., Gümren, M., Fenwick, A., Ertan, A., Bernstein, M., Amara, H. and Van Bavel, J. 2022. Predicting attitudinal and behavioral responses to COVID-19 pandemic using machine learning. PNAS Nexus. 1 (3), pp. 1-15. https://doi.org/10.1093/pnasnexus/pgac093

Adaptive weighted dynamic differential evolution algorithm for emergency material allocation and scheduling

Wang, T., Wu, K., Du, T. and Cheng, X. 2022. Adaptive weighted dynamic differential evolution algorithm for emergency material allocation and scheduling. Computational Intelligence. 38 (3), pp. 714-730. https://doi.org/10.1111/coin.12389

Explanation by automated reasoning using the Isabelle Infrastructure framework

Kammueller, F. 2022. Explanation by automated reasoning using the Isabelle Infrastructure framework. Chen, J.Y.C., Fragomeni, G., Degen, H. and Ntoa, S. (ed.) HCII 2022: 24th International Conference on Human-Computer Interaction. Virtual 26 Jun - 01 Jul 2022 Springer. pp. 307-318 https://doi.org/10.1007/978-3-031-21707-4_22

National identity predicts public health support during a global pandemic

Van Bavel, J., Cichocka, A., Capraro, V., Sjåstad, H., Nezlek, J., Pavlović, T., Alfano, M., Gelfand, M., Azevedo, F., Birtel, M., Cislak, A., Lockwood, P., Ross, R., Abts, K., Agadullina, E., Aruta, J., Besharati, S., Bor, A., Choma, B., Crabtree, C., Cunningham, W., De, K., Ejaz, W., Elbaek, C., Findor, A., Flichtentrei, D., Franc, R., Gjoneska, B., Gruber, J., Gualda, E., Horiuchi, Y., Huynh, T., Ibanez, A., Imran, M., Israelashvili, J., Jasko, K., Kantorowicz, J., Kantorowicz-Reznichenko, E., Krouwel, A., Laakasuo, M., Lamm, C., Leygue, C., Lin, M., Mansoor, M., Marie, A., Mayiwar, L., Mazepus, H., McHugh, C., Minda, J., Mitkidis, P., Olsson, A., Otterbring, T., Packer, D., Perry, A., Petersen, M., Puthillam, A., Riaño-Moreno, J., Rothmund, T., Santamaría-García, H., Schmid, P., Stoyanov, D., Tewari, S., Todosijević, B., Tsakiris, M., Tung, H., Umbreș, R., Vanags, E., Vlasceanu, M., Vonasch, A., Yucel, M., Zhang, Y., Abad, M., Adler, E., Akrawi, N., Mdarhri, H., Amara, H., Amodio, D., Antazo, B., Apps, M., Ay, F., Ba, M., Barbosa, S., Bastian, B., Berg, A., Bernal-Zárate, M., Bernstein, M., Białek, M., Bilancini, E., Bogatyreva, N., Boncinelli, L., Booth, J., Borau, S., Buchel, O., Cameron, C., Carvalho, C., Celadin, T., Cerami, C., Chalise, H., Cheng, X., Cian, L., Cockcroft, K., Conway, J., Córdoba-Delgado, M., Crespi, C., Crouzevialle, M., Cutler, J., Cypryańska, M., Dabrowska, J., Daniels, M., Davis, V., Dayley, P., Delouvee, S., Denkovski, O., Dezecache, G., Dhaliwal, N., Diato, A., Di Paolo, R., Drosinou, M., Dulleck, U., Ekmanis, J., Ertan, A., Etienne, T., Farhana, H., Farkhari, F., Farmer, H., Fenwick, A., Fidanovski, K., Flew, T., Fraser, S., Frempong, R., Fugelsang, J., Gale, J., Garcia-Navarro, E., Garladinne, P., Ghajjou, O., Gkinopoulos, T., Gray, K., Griffin, S., Gronfeldt, B., Gümren, M., Gurung, R., Halperin, E., Harris, E., Herzon, V., Hruška, M., Huang, G., Hudecek, M., Isler, O., Jangard, S., Jørgensen, F., Kachanoff, F., Kahn, J., Dangol, A., Keudel, O., Koppel, L., Koverola, M., Kubin, E., Kunnari, A., Kutiyski, Y., Laguna, O., Leota, J., Lermer, E., Levy, J., Levy, N., Li, C., Long, E., Longoni, C., Maglić, M., McCashin, D., Metcalf, A., Mikloušić, I., El Mimouni, S., Miura, A., Molina-Paredes, J., Monroy-Fonseca, C., Morales-Marente, E., Moreau, D., Muda, R., Myer, A., Nash, K., Nesh-Nash, T., Nitschke, J., Nurse, M., Ohtsubo, Y., Oldemburgo de Mello, V., O’Madagain, C., Onderco, M., Palacios-Galvez, M., Palomäki, J., Pan, Y., Papp, Z., Pärnamets, P., Paruzel-Czachura, M., Pavlović, Z., Payán-Gómez, C., Perander, S., Pitman, M., Prasad, R., Pyrkosz-Pacyna, J., Rathje, S., Raza, A., Rêgo, G., Rhee, K., Robertson, C., Rodríguez-Pascual, I., Saikkonen, T., Salvador-Ginez, O., Sampaio, W., Santi, G., Santiago-Tovar, N., Savage, D., Scheffer, J., Schönegger, P., Schultner, D., Schutte, E., Scott, A., Sharma, M., Sharma, P., Skali, A., Stadelmann, D., Stafford, C., Stanojević, D., Stefaniak, A., Sternisko, A., Stoica, A., Stoyanova, K., Strickland, B., Sundvall, J., Thomas, J., Tinghög, G., Torgler, B., Traast, I., Tucciarelli, R., Tyrala, M., Ungson, N., Uysal, M., Van Lange, P., van Prooijen, J., van Rooy, D., Västfjäll, D., Verkoeijen, P., Vieira, J., von Sikorski, C., Walker, A., Watermeyer, J., Wetter, E., Whillans, A., Willardt, R., Wohl, M., Wójcik, A., Wu, K., Yamada, Y., Yilmaz, O., Yogeeswaran, K., Ziemer, C., Zwaan, R. and Boggio, P. 2022. National identity predicts public health support during a global pandemic. Nature Communications. 13 (1), pp. 1-14. https://doi.org/10.1038/s41467-021-27668-9

CroLSSim: Cross‐language software similarity detector using hybrid approach of LSA‐based AST‐MDrep features and CNN‐LSTM model

Ullah, F., Naeem, M., Naeem, H., Cheng, X. and Alazab, M. 2022. CroLSSim: Cross‐language software similarity detector using hybrid approach of LSA‐based AST‐MDrep features and CNN‐LSTM model. International Journal of Intelligent Systems. 37 (9), pp. 5768-5795. https://doi.org/10.1002/int.22813

MobiScan: an enhanced invisible screen‐camera communication system for IoT applications

Zhang, X., Liu, J., Ba, Z., Tao, Y. and Cheng, X. 2022. MobiScan: an enhanced invisible screen‐camera communication system for IoT applications. Transactions on Emerging Telecommunications Technologies. 33 (4). https://doi.org/10.1002/ett.4151

Secure smart contracts for cloud-based manufacturing using Ethereum blockchain

Kumar, A., Abhishek, K., Nerurkar, P., Ghalib, M., Shankar, A. and Cheng, X. 2022. Secure smart contracts for cloud-based manufacturing using Ethereum blockchain. Transactions on Emerging Telecommunications Technologies. 33 (4). https://doi.org/10.1002/ett.4129

Dependability engineering in Isabelle

Kammueller, F. 2021. Dependability engineering in Isabelle. arxiv.org.

Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders

Kammueller, F. and Alvarado, C. 2021. Exploring rationality of self awareness in social networking for logical modeling of unintentional insiders. arxiv.org.

Editorial: Security of cloud service for the manufacturing industry

Cheng, X., Liu, Z. and Ning, Y. 2022. Editorial: Security of cloud service for the manufacturing industry. Transactions on Emerging Telecommunications Technologies. 33 (4). https://doi.org/10.1002/ett.4369

Power grid-oriented cascading failure vulnerability identifying method based on wireless sensors

Li, S., Chen, Y., Wu, X., Cheng, X. and Tian, Z. 2021. Power grid-oriented cascading failure vulnerability identifying method based on wireless sensors. Journal of Sensors. 2021, pp. 1-12. https://doi.org/10.1155/2021/8820413

Secure and energy-efficient smart building architecture with emerging technology IoT

Kumar, A., Sharma, S., Goyal, N., Singh, A., Cheng, X. and Singh, P. 2021. Secure and energy-efficient smart building architecture with emerging technology IoT. Computer Communications. 176, pp. 207-217. https://doi.org/10.1016/j.comcom.2021.06.003

Fuzzy decision trees embedded with evolutionary fuzzy clustering for locating users using wireless signal strength in an indoor environment

Narayanan, S., Baby, C., Perumal, B., Bhatt, R., Cheng, X., Ghalib, M. and Shankar, A. 2021. Fuzzy decision trees embedded with evolutionary fuzzy clustering for locating users using wireless signal strength in an indoor environment. International Journal of Intelligent Systems. 36 (8), pp. 4280-4267. https://doi.org/10.1002/int.22459

PSSPNN: PatchShuffle Stochastic Pooling Neural Network for an explainable diagnosis of COVID-19 with multiple-way data augmentation

Wang, S., Zhang, Y., Cheng, X., Zhang, X. and Zhang, Y. 2021. PSSPNN: PatchShuffle Stochastic Pooling Neural Network for an explainable diagnosis of COVID-19 with multiple-way data augmentation. Computational and Mathematical Methods in Medicine. 2021, pp. 1-18. https://doi.org/10.1155/2021/6633755

Modeling and verifying a resource allocation algorithm for secure service migration for commercial cloud systems

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2022. Modeling and verifying a resource allocation algorithm for secure service migration for commercial cloud systems. Computational Intelligence. 38 (3), pp. 811-828. https://doi.org/10.1111/coin.12421

Applying the Isabelle insider framework to airplane security

Kammueller, F. and Kerber, M. 2021. Applying the Isabelle insider framework to airplane security. Science of Computer Programming. 206. https://doi.org/10.1016/J.SCICO.2021.102623

Task bundling in worker-centric mobile crowdsensing

Zhao, T., Yang, Y., Wang, E., Mumtaz, S. and Cheng, X. 2021. Task bundling in worker-centric mobile crowdsensing. International Journal of Intelligent Systems. 36 (9), pp. 4936-4961. https://doi.org/10.1002/int.22497

ShadowFPE: new encrypted web application solution based on shadow DOM

Guo, X., Huang, Y., Ye, J., Yin, S., Li, M., Li, Z., Yiu, S. and Cheng, X. 2021. ShadowFPE: new encrypted web application solution based on shadow DOM. Mobile Networks and Applications. 26 (4), pp. 1733-1746. https://doi.org/10.1007/s11036-019-01509-y

Masterminding change by combining secure system design with security risk assessment

Kammueller, F., Legay, A. and Schivo, S. 2021. Masterminding change by combining secure system design with security risk assessment. International Journal on Software Tools for Technology Transfer. 23 (1), pp. 69-70. https://doi.org/10.1007/s10009-020-00595-8

Combining secure system design with risk assessment for IoT healthcare systems

Kammueller, F. 2019. Combining secure system design with risk assessment for IoT healthcare systems. SPT-IoT'19 - The Third Workshop on Security, Privacy and Trust in the Internet of Things, colocated with IEEE PerCom 2019. Kyoto, Japan 11 - 15 Mar 2019 Institute of Electrical and Electronics Engineers (IEEE). pp. 961-966 https://doi.org/10.1109/PERCOMW.2019.8730776

Learning context-aware outfit recommendation

Abugabah, A., Cheng, X. and Wang, J. 2020. Learning context-aware outfit recommendation. Symmetry. 12 (6), pp. 1-13. https://doi.org/10.3390/sym12060873

Renyi’s entropy based multilevel thresholding using a novel meta-heuristics algorithm

Liu, W., Huang, Y., Ye, Z., Cai, W., Yang, S., Cheng, X. and Frank, I. 2020. Renyi’s entropy based multilevel thresholding using a novel meta-heuristics algorithm. Applied Sciences. 10 (9). https://doi.org/10.3390/app10093225

Reliability analysis of an air traffic network: from network structure to transport function

Li, S., Zhang, Z. and Cheng, X. 2020. Reliability analysis of an air traffic network: from network structure to transport function. Applied Sciences. 10 (9). https://doi.org/10.3390/app10093168

XOR multiplexing technique for nanocomputers

Yu, L., Diao, M., Chen, X. and Cheng, X. 2020. XOR multiplexing technique for nanocomputers. Applied Sciences. 10 (8). https://doi.org/10.3390/app10082825

Fine-grained action recognition by motion saliency and mid-level patches

Liu, F., Zhao, L., Cheng, X., Dai, Q., Shi, X. and Qiao, J. 2020. Fine-grained action recognition by motion saliency and mid-level patches. Applied Sciences. 10 (8). https://doi.org/10.3390/app10082811

Adaptive dynamic disturbance strategy for differential evolution algorithm

Wang, T., Wu, K., Du, T. and Cheng, X. 2020. Adaptive dynamic disturbance strategy for differential evolution algorithm. Applied Sciences. 10 (6). https://doi.org/10.3390/app10061972

Hybridization of cognitive computing for food services

Zhang, X., Yang, S., Srivastava, G., Chen, M. and Cheng, X. 2020. Hybridization of cognitive computing for food services. Applied Soft Computing. 89. https://doi.org/10.1016/j.asoc.2019.106051

Cloud resource prediction model based on triple exponential smoothing method and temporal convolutional network

Xie, X., Zhang, Z., Wang, J. and Cheng, X. 2019. Cloud resource prediction model based on triple exponential smoothing method and temporal convolutional network. Journal on Communications. 40 (8), pp. 143-150. https://doi.org/10.11959/j.issn.1000-436x.2019172

Incremental association rule mining based on matrix compression for edge computing

Zhou, D., Ouyang, M., Kuang, Z., Li, Z., Zhou, J. and Cheng, X. 2019. Incremental association rule mining based on matrix compression for edge computing. IEEE Access. 7, pp. 1730444-173053. https://doi.org/10.1109/ACCESS.2019.2956823

Facial landmark detection via attention-adaptive deep network

Sadiq, M., Shi, D., Guo, M. and Cheng, X. 2019. Facial landmark detection via attention-adaptive deep network. IEEE Access. 7, pp. 181041-181050. https://doi.org/10.1109/ACCESS.2019.2955156

Annual and non-monsoon rainfall prediction modelling using SVR-MLP: an empirical study from Odisha

Yhang, X., Mohanty, S., Parida, A., Pani, S., Dong, B. and Cheng, X. 2020. Annual and non-monsoon rainfall prediction modelling using SVR-MLP: an empirical study from Odisha. IEEE Access. 8, pp. 30223-30233. https://doi.org/10.1109/ACCESS.2020.2972435

A sparse Bayesian learning method for structural equation model-based gene regulatory network inference

Li, Y., Liu, D., Chu, J., Zhu, Y., Liu, J. and Cheng, X. 2020. A sparse Bayesian learning method for structural equation model-based gene regulatory network inference. IEEE Access. 8, pp. 40067-40080. https://doi.org/10.1109/ACCESS.2020.2976743

Modeling and analyzing the Corona-virus warning app with the Isabelle infrastructure framework

Kammueller, F. and Lutz, B. 2020. Modeling and analyzing the Corona-virus warning app with the Isabelle infrastructure framework. Garcia-Alfaro, J., Navarro-Arribas, G. and Herrera-Joancomarti, J. (ed.) International Workshop of Data Privacy Management, DPM'20. University of Surrey, UK 17 - 18 Sep 2020 Springer. pp. 128-144 https://doi.org/10.1007/978-3-030-66172-4_8

Inter-blockchain protocols with the Isabelle Infrastructure framework

Kammueller, F. and Nestmann, U. 2020. Inter-blockchain protocols with the Isabelle Infrastructure framework. Bernardo, B. and Marmsoler, D. (ed.) 2nd Workshop on Formal Methods for Blockchain, co-located with CAV'20. Los Angeles, CA, USA Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH. pp. 11:1-11:12 https://doi.org/10.4230/OASIcs.FMBC.2020.11

A formal development cycle for security engineering in Isabelle

Kammueller, F. 2020. A formal development cycle for security engineering in Isabelle. arxiv.org. https://doi.org/10.48550/arXiv.2001.08983

Applying the Isabelle Insider framework to airplane security

Kammueller, F. and Kerber, M. 2020. Applying the Isabelle Insider framework to airplane security. arxiv.org. https://doi.org/10.48550/arXiv.2003.11838

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

Kammueller, F. 2020. Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems.

A game theoretic analysis of resource mining in blockchain

Singh, R., Dwivedi, A., Srivastava, G., Wisznieska-Mayszkiel, A. and Cheng, X. 2020. A game theoretic analysis of resource mining in blockchain. Cluster Computing. 23 (3), pp. 2035-2046. https://doi.org/10.1007/s10586-020-03046-w

Describing and simulating concurrent quantum systems

Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16

Micro-distortion detection of lidar scanning signals based on geometric analysis

Liu, S., Chen, X., Li, Y. and Cheng, X. 2019. Micro-distortion detection of lidar scanning signals based on geometric analysis. Symmetry. 11 (12), pp. 2-13. https://doi.org/10.3390/sym11121471

Verifying cryptographic protocols

Ma, X. and Cheng, X. 2005. Verifying cryptographic protocols. IEEE Journal of Intelligent Cybernetic Systems.

Verifying security protocols by knowledge analysis

Ma, X. and Cheng, X. 2008. Verifying security protocols by knowledge analysis. International Journal of Security and Networks. 3 (3), pp. 183-192. https://doi.org/10.1504/IJSN.2008.020092

A face recognition algorithm using a fusion method based on Adaboost Bidirectional 2DLDA

Wang, S., Li, W., Cheng, X., Wang, Y. and Jiang, Y. 2012. A face recognition algorithm using a fusion method based on Adaboost Bidirectional 2DLDA. Advances in Information Sciences and Service Sciences. 4 (23), pp. 181-188. https://doi.org/10.4156/AISS.vol4.issue23.23

A security design for cloud computing: an implementation of an on premises authentication with Kerberos and IPSec within a network

Umar, M. and Cheng, X. 2012. A security design for cloud computing: an implementation of an on premises authentication with Kerberos and IPSec within a network. International Journal of Advanced Research in Computer Science. 3 (1), pp. 10-16. https://doi.org/10.26483/ijarcs.v3i1.6040

Comparative experiments on resource discovery in P2P networks

Gautam, S. and Cheng, X. 2014. Comparative experiments on resource discovery in P2P networks. Journal of Next Generation Information Technology. 5 (1), pp. 89-98.

Unbalanced private set intersection cardinality protocol with low communication cost

Lv, S., Ye, J., Yin, S. and Cheng, X. 2020. Unbalanced private set intersection cardinality protocol with low communication cost. Future Generation Computer Systems. 102, pp. 1054-1061. https://doi.org/10.1016/j.future.2019.09.022

Finding sands in the eyes: vulnerabilities discovery in IoT with EUFuzzer on human machine interface

Men, J., Xu, G., Han, Z., Sun, Z., Zhou, X., Lian, W. and Cheng, X. 2019. Finding sands in the eyes: vulnerabilities discovery in IoT with EUFuzzer on human machine interface. IEEE Access. 7, pp. 103751-103759. https://doi.org/10.1109/ACCESS.2019.2931061

Behavior modelling and individual recognition of sonar transmitter for secure communication in UASNs

Shi, F., Chen, Z. and Cheng, X. 2020. Behavior modelling and individual recognition of sonar transmitter for secure communication in UASNs. IEEE Access. 8, pp. 2447-2454. https://doi.org/10.1109/ACCESS.2019.2923059

Exploring a security protocol for secure service migration in commercial cloud environments

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2017. Exploring a security protocol for secure service migration in commercial cloud environments. ICC’17. Cambridge University, Cambridge 22 Mar 2019 ICC’17, Cambridge, United Kingdom © 2017 ACM.. pp. 1-6 https://doi.org/10.1145/3018896.3056795

Introduction of key problems in long-distance learning and training

Liu, S., Li, Z., Zhang, Y. and Cheng, X. 2019. Introduction of key problems in long-distance learning and training. Mobile Networks and Applications. 24 (1), pp. 1-4. https://doi.org/10.1007/s11036-018-1136-6

Vulnerabilities and limitations of MQTT protocol used between IoT devices

Dinculeană, D. and Cheng, X. 2019. Vulnerabilities and limitations of MQTT protocol used between IoT devices. Applied Sciences. 9 (5). https://doi.org/10.3390/app9050848

Imbalanced big data classification based on virtual reality in cloud computing

Xie, W. and Cheng, X. 2020. Imbalanced big data classification based on virtual reality in cloud computing. Multimedia Tools and Applications. 79 (23-24), pp. 16403-16420. https://doi.org/10.1007/s11042-019-7317-x

Platform of quality evaluation system for multimedia video communication based NS2

Yu, G., Xu, J. and Cheng, X. 2018. Platform of quality evaluation system for multimedia video communication based NS2. Journal of Ambient Intelligence and Humanized Computing. https://doi.org/10.1007/s12652-018-1164-x

Attack trees in Isabelle

Kammueller, F. 2018. Attack trees in Isabelle. 20th International Conference on Information and Communications Security, ICICS 2018. Lille, France 29 - 31 Oct 2018 Springer. pp. 611-628 https://doi.org/10.1007/978-3-030-01950-1_36

An authentication scheme to defend against UDP DrDoS attacks in 5G networks

Huang, H., Hu, L., Chu, J. and Cheng, X. 2019. An authentication scheme to defend against UDP DrDoS attacks in 5G networks. IEEE Access. 7, pp. 175970-175979. https://doi.org/10.1109/ACCESS.2019.2957565

Attack trees in Isabelle extended with probabilities for Quantum Cryptography

Kammueller, F. 2019. Attack trees in Isabelle extended with probabilities for Quantum Cryptography. Computers and Security. 87. https://doi.org/10.1016/j.cose.2019.101572

Data provenance with retention of reference relations

Wang, C., Yang, L., Wu, Y., Wu, Y., Cheng, X., Li, Z. and Liu, Z. 2018. Data provenance with retention of reference relations. IEEE Access. https://doi.org/10.1109/ACCESS.2018.2876879

Edit distance Kernelization of NP theorem proving for polynomial-time machine learning of proof heuristics

Windridge, D. and Kammueller, F. 2020. Edit distance Kernelization of NP theorem proving for polynomial-time machine learning of proof heuristics. FICC 2019: Future of Information and Communications Conference. San Francisco, USA 14 - 15 Mar 2019 Springer. pp. 271-283 https://doi.org/10.1007/978-3-030-12385-7_22

Formal modeling and analysis of data protection for GDPR compliance of IoT healthcare systems

Kammueller, F. 2018. Formal modeling and analysis of data protection for GDPR compliance of IoT healthcare systems. IEEE SMC 2018: IEEE International Conference on Systems, Man and Cybernetics. Miyazaki, Japan 08 - 10 Oct 2018 Institute of Electrical and Electronics Engineers (IEEE).

Editorial: Recent advances of content understanding in image and multimedia

Liu, S., Cheng, X. and Min, G. 2017. Editorial: Recent advances of content understanding in image and multimedia. Recent Patents on Computer Science. 10 (1), pp. 2-5. https://doi.org/10.2174/221327591001170808093310

Channel state information-based detection of Sybil attacks in wireless networks

Wang, C., Zhu, L., Gong, L., Zhao, Z., Yang, L., Liu, Z. and Cheng, X. 2018. Channel state information-based detection of Sybil attacks in wireless networks. Journal of Internet Services and Information Security. 8 (1), pp. 2-17. https://doi.org/10.22667/JISIS.2018.02.28.002

Formalization and analysis of a resource allocation security protocol for secure service migration

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2018. Formalization and analysis of a resource allocation security protocol for secure service migration. IEEE/ACM International Conference on Utility and Cloud Computing (UCC2018). Zurich, Switzerland 17 - 20 Dec 2018 IEEE. pp. 207-212 https://doi.org/10.1109/UCC-Companion.2018.00058

Research on trust model in container-based cloud service

Xie, X., Yuan, T., Zhou, X. and Cheng, X. 2018. Research on trust model in container-based cloud service. Computers, Materials and Continua. 56 (2), pp. 273-283. https://doi.org/10.3970/cmc.2018.03587

Introduction of recent advanced hybrid information processing

Liu, S., Li, Z., Cheng, X. and Lin, Y. 2018. Introduction of recent advanced hybrid information processing. Mobile Networks and Applications. 23 (4), pp. 673-676. https://doi.org/10.1007/s11036-018-1013-3

Accurate Sybil attack detection based on fine-grained physical channel information

Wang, C., Zhu, L., Gong, L., Zhao, Z., Yang, L., Liu, Z. and Cheng, X. 2018. Accurate Sybil attack detection based on fine-grained physical channel information. Sensors. 18 (3). https://doi.org/10.3390/s18030878

DivORAM: Towards a practical oblivious RAM with variable block size

Liu, Z., Huang, Y., Li, J., Cheng, X. and Shen, C. 2018. DivORAM: Towards a practical oblivious RAM with variable block size. Information Sciences. 447, pp. 1-11. https://doi.org/10.1016/j.ins.2018.02.071

M-SSE: an effective searchable symmetric encryption with enhanced security for mobile devices

Gao, C., Lv, S., Wei, Y., Wang, Z., Liu, Z. and Cheng, X. 2018. M-SSE: an effective searchable symmetric encryption with enhanced security for mobile devices. IEEE Access. 6, pp. 38860-38869. https://doi.org/10.1109/ACCESS.2018.2852329

A distributed anomaly detection system for in-vehicle network using HTM

Wang, C., Zhao, Z., Gong, L., Zhu, L., Liu, Z. and Cheng, X. 2018. A distributed anomaly detection system for in-vehicle network using HTM. IEEE Access. 6, pp. 9091-9098. https://doi.org/10.1109/ACCESS.2018.2799210

Crime pattern recognition based on high-performance computing

Eissa, A., Cheng, X. and Petridis, M. 2018. Crime pattern recognition based on high-performance computing. 2017 International Conference Next Generation Community Policing. Heraklion, Crete, Greece 25 - 27 Oct 2017

A proof calculus for attack trees in Isabelle

Kammueller, F. 2017. A proof calculus for attack trees in Isabelle. 12th International Workshop on Data Privacy Management (DPM 2017). Oslo, Norway 14 - 15 Sep 2017 Springer. pp. 3-18 https://doi.org/10.1007/978-3-319-67816-0_1

Exploring a security protocol for secure service migration in commercial cloud environments

Karthick, G., Mapp, G., Kammueller, F. and Aiash, M. 2017. Exploring a security protocol for secure service migration in commercial cloud environments. 2nd International Conference on Internet of Things, Data and Cloud Computing (ICC 2017). Churchill College, University of Cambridge, United Kingdom 22 - 23 Mar 2017 Association for Computing Machinery (ACM). https://doi.org/10.1145/3018896.3056795

Model based analysis of insider threats

Chen, T., Han, T., Kammueller, F., Nemli, I. and Probst, C. 2016. Model based analysis of insider threats. 2016 International Conference on Cyber Security and Protection of Digital Services (Cyber Security). London, United Kingdom 13 - 14 Jun 2016 Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/CyberSecPODS.2016.7502350

Security and privacy requirements engineering for human centric IoT systems using eFRIEND and Isabelle

Kammueller, F., Augusto, J. and Jones, S. 2017. Security and privacy requirements engineering for human centric IoT systems using eFRIEND and Isabelle. IEEE/ACIS 15th International Conference on Software Engineering Research, Management and Application, SERA2017. University of Greenwich, London, United Kingdom 07 - 09 Jun 2017 Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/SERA.2017.7965758

Formal modeling and analysis with humans in infrastructures for IoT health care systems

Kammueller, F. 2017. Formal modeling and analysis with humans in infrastructures for IoT health care systems. 5th International Conference on Human Aspects of Security, Privacy and Trust, HCII-HAS 2017. Vancouver, BC, Canada 09 - 14 Jul 2017 Springer. pp. 339-352 https://doi.org/10.1007/978-3-319-58460-7_24

Human centric security and privacy for the IoT using formal techniques

Kammueller, F. 2018. Human centric security and privacy for the IoT using formal techniques. 3rd International Conference on Human Factors in Cybersecurity. Los Angeles, CA, United States 17 - 21 Jul 2017 Springer. pp. 106-116 https://doi.org/10.1007/978-3-319-60585-2_12

Insider threats for auctions: formalization, mechanized proof, and code generation

Kammueller, F., Kerber, M. and Probst, C. 2017. Insider threats for auctions: formalization, mechanized proof, and code generation. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA). 8 (1), pp. 44-78. https://doi.org/10.22667/JOWUA.2017.03.31.044

A novel fast fractal image compression method based on distance clustering in high dimensional sphere surface

Liu, S., Pan, Z. and Cheng, X. 2017. A novel fast fractal image compression method based on distance clustering in high dimensional sphere surface. Fractals. 25 (04), pp. 1740004-1-11. https://doi.org/10.1142/s0218348x17400047

Modeling and verification of insider threats using logical analysis

Kammueller, F. and Probst, C. 2017. Modeling and verification of insider threats using logical analysis. IEEE Systems Journal. 11 (2), pp. 534-545. https://doi.org/10.1109/JSYST.2015.2453215

Towards formal analysis of insider threats for auctions

Kammueller, F., Kerber, M. and Probst, C. 2016. Towards formal analysis of insider threats for auctions. ACM-CCS Workshop on Management of Security of Insider Threats. Vienna, Austria 28 Oct 2016 Association for Computing Machinery (ACM). pp. 23-34 https://doi.org/10.1145/2995959.2995963

Isabelle Modelchecking for insider threats

Kammueller, F. 2016. Isabelle Modelchecking for insider threats. 11th DPM International Workshop on Data Privacy Management (DPM 2016) co-located with ESORICS 2016. Heraklion, Crete, Greece 26 - 27 Sep 2016 Springer. pp. 196-210 https://doi.org/10.1007/978-3-319-47072-6_13

Refactoring preserves security

Kammueller, F. 2016. Refactoring preserves security. 11th DPM International Workshop on Data Privacy Management (DPM 2016) co-located with ESORICS 2016. Heraklion, Crete, Greece 26 - 27 Sep 2016 Springer. pp. 238-245 https://doi.org/10.1007/978-3-319-47072-6_17

Verification of statecharts using data abstraction

Helke, S. and Kammueller, F. 2016. Verification of statecharts using data abstraction. International Journal of Advanced Computer Science and Applications. 7 (1), pp. 571-583. https://doi.org/10.14569/IJACSA.2016.070179

Formal modelling and analysis of socio-technical systems

Probst, C., Kammueller, F. and Hansen, R. 2016. Formal modelling and analysis of socio-technical systems. in: Semantics, Logics, and Calculi Springer International.

Attack tree analysis for insider threats on the IoT using Isabelle

Kammueller, F., Nurse, J. and Probst, C. 2016. Attack tree analysis for insider threats on the IoT using Isabelle. 4th International Conference on Human Aspects of Security, Privacy and Trust, HCII-HAS 2016. Toronto, ON, Canada 17 - 24 Jul 2016 Springer International. pp. 234-246 https://doi.org/10.1007/978-3-319-39381-0_21

Degradation and encryption for outsourced PNG images in cloud storage

Wang, Y., Du, J., Cheng, X., Liu, Z. and Lin, K. 2016. Degradation and encryption for outsourced PNG images in cloud storage. International Journal of Grid and Utility Computing. 7 (1), pp. 22-28. https://doi.org/10.1504/IJGUC.2016.073773

Trust-Driven and PSO-SFLA based job scheduling algorithm on Cloud

Xie, X., Liu, R., Cheng, X., Hu, X. and Ni, J. 2016. Trust-Driven and PSO-SFLA based job scheduling algorithm on Cloud. Intelligent Automation & Soft Computing: An International Journal . 22 (4), pp. 561-566.

Investigating airplane safety and security against insider threats using logical modeling

Kammueller, F. and Kerber, M. 2016. Investigating airplane safety and security against insider threats using logical modeling. 2016 IEEE Security and Privacy Workshops SPW'16: Workshop on Research in Insider Threats WRIT'16. San Jose, CA, USA 22 - 26 May 2016 Institute of Electrical and Electronics Engineers (IEEE). pp. 304-313 https://doi.org/10.1109/SPW.2016.47

Secure refactoring with Java information flow

Helke, S., Kammueller, F. and Probst, C. 2016. Secure refactoring with Java information flow. 10th International Workshop on Data Privacy Management (DPM 2015). Vienna, Austria 21 - 22 Sep 2015 Springer. pp. 264-272 https://doi.org/10.1007/978-3-319-29883-2_19

Transforming graphical system models to graphical attack models

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2016. Transforming graphical system models to graphical attack models. 2nd International Workshop on Graphical Models for Security, GraMSec 2015, co-located with CSF2015. Verona, Italy 13 Jul 2015 Springer. pp. 82-96 https://doi.org/10.1007/978-3-319-29968-6_6

Attack tree generation by policy invalidation

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2015. Attack tree generation by policy invalidation. 9th WISTP International Conference on Information Security Theory and Practice (WISTP 2015). Heraklion, Crete, Greece 24 - 25 Aug 2015 Springer. pp. 249-259 https://doi.org/10.1007/978-3-319-24018-3_16

Formalization of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2015. Formalization of quantum protocols using Coq. The 12th International Workshop on Quantum Physics and Logic (QPL 2015). Oxford, United Kingdom 15 - 17 Jul 2015 pp. 71-83

Invalidating policies using structural information

Kammueller, F. and Probst, C. 2013. Invalidating policies using structural information. IEEE CS Security and Privacy Workshops, SPW, WRIT'13.

Network information flow control: proof of concept

Alghothami, A. and Kammueller, F. 2013. Network information flow control: proof of concept. IEEE Int. Conf. on Systems, Man, and Cybernetics, SMC. Manchester, UK 13 - 16 Oct 2013 IEEE. pp. 2957-2962 https://doi.org/10.1109/SMC.2013.504

Privacy analysis of a hidden friendship protocol

Kammueller, F. and Preibusch, S. 2013. Privacy analysis of a hidden friendship protocol. The 8th International Workshop on Data Privacy Management, DPM 2013. Egam, UK 12 - 13 Sep 2013 Springer. pp. 83-99

Externalizing behaviour for analysing system models

Ivanova, M., Probst, C., Hansen, R. and Kammueller, F. 2013. Externalizing behaviour for analysing system models. 5th International Workshop on Managing Insider Security Threats, MIST, 2013..

Verification of quantum protocols using Coq

Boender, J., Kammueller, F. and Nagarajan, R. 2014. Verification of quantum protocols using Coq. 17th Conference on Quantum Information Processing (QIP). Barcelona, Spain 03 - 07 Feb 2014

Reviews for the American Mathematical Society (AMS): Paul Howells, Mark d’Inverno. Specifying termination in CSP. Theoretical Computer Science, 503:31–61, 2013.

Kammueller, F. 2014. Reviews for the American Mathematical Society (AMS): Paul Howells, Mark d’Inverno. Specifying termination in CSP. Theoretical Computer Science, 503:31–61, 2013. MathSciNet: Mathematical Reviews.

Combining generated data models with formal invalidation for insider threat analysis

Kammueller, F. and Probst, C. 2014. Combining generated data models with formal invalidation for insider threat analysis. 2014 IEEE Security and Privacy Workshops (SPW): Workshop on Research for Insider Threat (WRIT 2014). San Jose, California, USA 17 - 18 May 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 229-235 https://doi.org/10.1109/SPW.2014.45

Verification of DNSsec delegation signatures

Kammueller, F. 2014. Verification of DNSsec delegation signatures. 21st International IEEE Conference on Telecommunication. Lisbon 04 - 07 May 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 298-392 https://doi.org/10.1109/ICT.2014.6845127

Invalidating policies using structural information

Kammueller, F. and Probst, C. 2014. Invalidating policies using structural information. Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications. 5 (2), pp. 59-79. https://doi.org/10.22667/JOWUA.2014.06.31.059

Modeling human behaviour with higher order logic: insider threats

Boender, J., Kammueller, F., Ivanova, M. and Primiero, G. 2014. Modeling human behaviour with higher order logic: insider threats. 4th Workshop on Socio-Technical Aspects in Security and Trust. Vienna Technical University, Vienna, Austria 18 Jul 2014 Institute of Electrical and Electronics Engineers (IEEE). pp. 31-39

A probabilistic analysis framework for malicious insider threats

Chen, T., Kammueller, F., Nemli, I. and Probst, C. 2015. A probabilistic analysis framework for malicious insider threats. 3rd International Conference on Human Aspects of Information Security, Privacy and Trust, HAS 2015, held as part of HCI International 2015. Los Angeles, California, USA 02 - 07 Aug 2015 Springer. pp. 178-189

Confinement for active objects

Kammueller, F. 2015. Confinement for active objects. International Journal of Advanced Computer Science and Applications. 6 (2), pp. 246-261. https://doi.org/10.14569/IJACSA.2015.060236

Modeling human behaviour with higher order logic: insider threats

Boender, J., Ivanova, M., Kammueller, F. and Primiero, G. 2014. Modeling human behaviour with higher order logic: insider threats. 4th Workshop on Socio-Technical Aspects in Security and Trust (STAST 2014). Vienna, Austria 18 Jul 2014 Institute of Electrical and Electronics Engineers. pp. 31-39 https://doi.org/10.1109/STAST.2014.13

Numeric characteristics of generalized M-set with its asymptote

Liu, S., Cheng, X., Fu, W., Zhou, Y. and Li, Q. 2014. Numeric characteristics of generalized M-set with its asymptote. Applied Mathematics and Computation. 243, pp. 767-774. https://doi.org/10.1016/j.amc.2014.06.016

Local semantic indexing for resource discovery on overlay network using mobile agents

Singh, M., Cheng, X. and Belavkin, R. 2014. Local semantic indexing for resource discovery on overlay network using mobile agents. International Journal of Computational Intelligence Systems. 7 (3), pp. 432-455. https://doi.org/10.1080/18756891.2013.856257

Fractal property of generalized M-set with rational number exponent

Liu, S., Cheng, X., Lan, C., Fu, W., Zhou, J., Li, Q. and Gao, G. 2013. Fractal property of generalized M-set with rational number exponent. Applied Mathematics and Computation. 220, pp. 668-675. https://doi.org/10.1016/j.amc.2013.06.096

Mechanical verification of cryptographic protocols

Cheng, X., Ma, X., Huang, S. and Cheng, M. 2010. Mechanical verification of cryptographic protocols. Network Security. https://doi.org/10.1007/978-0-387-73821-5_5

A semi-lattice model for multi-lateral security

Kammueller, F. 2013. A semi-lattice model for multi-lateral security. in: Data privacy management and autonomous spontaneous security Berlin, Germany Springer.

A security model for functional active objects

Kammueller, F. 2012. A security model for functional active objects. Francisco, C., Kim, V., Miguel, C. and Andreas, K. (ed.) First International Symposium Communicability, Computer Graphics and Innovative Design for Interactive Systems (CCGIDIS 2011). Berlin Springer. https://doi.org/10.1007/978-3-642-33760-4_4

A security model for functional active objects with an implementation in Erlang

Fleck, A. and Kammueller, F. 2011. A security model for functional active objects with an implementation in Erlang. in: Ficarra, F., Kratky, A., Veltman, K., Ficarra, M., Nicol, E. and Brie, M. (ed.) Computational informatics, social factors and new information technologies: hypermedia perspectives and avant-garde experiences in the era of communicability expansion Bergamo, Italy Blue Herons.

Engineering security protocols with modelchecking – Radius-SHA256 and secured simple protocol.

Kammueller, F., Mapp, G., Patel, S. and Sani, A. 2012. Engineering security protocols with modelchecking – Radius-SHA256 and secured simple protocol. International Conference on Internet Monitoring and Protection (ICIMP 2012). Stuttgart, Germany 27 May - 01 Jun 2012 Xpert Publishing Service.

Review for the American Mathematical Society (AMS): A. Francalanza et al. Permission-based separation logic for message-passing concurrency. Logical methods in computer science, 7: 1-47, 2011

Kammueller, F. 2012. Review for the American Mathematical Society (AMS): A. Francalanza et al. Permission-based separation logic for message-passing concurrency. Logical methods in computer science, 7: 1-47, 2011. Mathematical Reviews.

Reviews for the American Mathematical Society (AMS): Russell O’Connor. Classical mathematics for a constructive world. MSCS (21): 861–882, Cambridge University Press. 2010.

Kammueller, F. 2012. Reviews for the American Mathematical Society (AMS): Russell O’Connor. Classical mathematics for a constructive world. MSCS (21): 861–882, Cambridge University Press. 2010. Mathematical Reviews.

A locally nameless theory of objects

Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. A locally nameless theory of objects. SAFA Annual Workshop on Formal Techniques (SAFA’2010). 2229 Route des Crêtes, 06560, Valbonne, Provence-Alpes-Côte d'Azur, France

Locally nameless sigma calculus

Henrio, L., Kammueller, F., Lutz, B. and Sudhof, H. 2010. Locally nameless sigma calculus. Archive of Formal Proof.

Formalizing statecharts using hierarchical automata

Helke, S. and Kammueller, F. 2010. Formalizing statecharts using hierarchical automata. Archive of Formal Proof.

Radius-SHA256 – verified remote authentication with secure hashing.

Kammueller, F. and Patel, S. 2011. Radius-SHA256 – verified remote authentication with secure hashing. First Global Conference on Communication, Science and Information Engineering, CCSIE’11. Middlesex University 25 - 27 Jul 2011

ASPfun: a typed functional active object calculus

Henrio, L., Kammueller, F. and Lutz, B. 2012. ASPfun: a typed functional active object calculus. Science of Computer Programming. 77 (7-8), pp. 823-847. https://doi.org/10.1016/j.scico.2010.12.008

Application of verification techniques to security: model checking insider attacks

Kammueller, F., Probst, C. and Raimondi, F. 2012. Application of verification techniques to security: model checking insider attacks. 1st International Conference on Software and Emerging Technologies for Education, Culture, Entertainment, and Commerce (SETECEC 2012): New Directions in Multimedia Mobile Computing, Social Networks, Human-Computer Interaction and Communicability. Venice, Italy 28 - 29 Mar 2012 Blue Herons editions.

A cooperative particle swarm optimizer with statistical variable interdependence learning

Sun, L., Yoshida, S., Cheng, X. and Liang, Y. 2012. A cooperative particle swarm optimizer with statistical variable interdependence learning. Information Sciences. 186 (1), pp. 20-39. https://doi.org/10.1016/j.ins.2011.09.033

Survey of grid resource monitoring and prediction strategies.

Hu, L., Cheng, X. and Che, X. 2010. Survey of grid resource monitoring and prediction strategies. International Journal of Intelligent Information Processing. 1 (2).

Efficient identity-based broadcast encryption without random oracles.

Hu, L., Liu, Z. and Cheng, X. 2010. Efficient identity-based broadcast encryption without random oracles. Journal of Computers. 5 (3), pp. 331-336.

Solving job shop scheduling problem using genetic algorithm with penalty function

Sun, L., Cheng, X. and Liang, Y. 2010. Solving job shop scheduling problem using genetic algorithm with penalty function. International Journal of Intelligent Information Processing. 1 (2), pp. 65-77.

Modelchecking non-functional requirements for interface specifications.

Kammueller, F. and Preibusch, S. 2008. Modelchecking non-functional requirements for interface specifications. European Joint Conference on Theory and Practice of Software, 2008, (Foundations of Interface technologies). Budapest 29 Mar - 06 Apr 2008

Compositionality of aspect weaving.

Kammueller, F. and Sudhof, H. 2008. Compositionality of aspect weaving. in: Mahr, B. and Sheng, H. (ed.) Autonomous systems: self-organisation, management, and control. Springer Verlag. pp. 87-96

Interactive theorem proving in software engineering.

Kammueller, F. 2008. Interactive theorem proving in software engineering. Saarbrücken, Germany VDM Verlag Dr. Mueller.

Using functional active objects to enforce privacy

Kammueller, F. 2010. Using functional active objects to enforce privacy. 5th Conference on Network Architectures and Information Systems Security. Menton, France 18 - 21 May 2010

Enhancing privacy implementations of database enquiries

Kammueller, F. and Kammueller, R. 2009. Enhancing privacy implementations of database enquiries. IEEE. pp. 45-50 https://doi.org/10.1109/ICIMP.2009.15

Implementing privacy with Erlang active objects

Fleck, A. and Kammueller, F. 2010. Implementing privacy with Erlang active objects. International Conference on Internet Monitoring and Protection. Barcelona 09 - 15 May 2010 IEEE. pp. 141-146 https://doi.org/10.1109/ICIMP.2010.27

Privacy by flexible parameterization with Erlang active objects.

Fleck, A. and Kammueller, F. 2010. Privacy by flexible parameterization with Erlang active objects. International Journal on Advances in Software. 3 (3-4), pp. 461-473.

Functional active objects: typing and formalisation

Henrio, L. and Kammueller, F. 2009. Functional active objects: typing and formalisation. Elsevier. https://doi.org/10.1016/j.entcs.2009.10.026

Feature link propagation across variability representations with Isabelle/HOL

Kammueller, F., Rein, A. and Reiser, M. 2010. Feature link propagation across variability representations with Isabelle/HOL. Rubin, J., Botterweck, G., Mezini, M., Maman, I. and Lero, A. (ed.) New York Association for Computing Machinery (ACM). pp. 48-53

Checking the TWIN elevator system by translating object-Z to SMV

Preibusch, S. and Kammueller, F. 2008. Checking the TWIN elevator system by translating object-Z to SMV. Lecture Notes in Computer Science. 4916, pp. 38-55. https://doi.org/10.1007/978-3-540-79707-4

Composing safely: a type system for aspects

Kammueller, F. and Sudhof, H. 2008. Composing safely: a type system for aspects. Lecture Notes in Computer Science. 4954, pp. 231-247. https://doi.org/10.1007/978-3-540-78789-1_18

Security analysis of private data enquiries in Erlang

Kammueller, F. and Kammueller, R. 2009. Security analysis of private data enquiries in Erlang. International Journal on Advances in Security. 2 (2&3), pp. 242-255.

An asynchronous distributed component model and its semantics

Henrio, L., Kammueller, F. and Rivera, M. 2009. An asynchronous distributed component model and its semantics. Lecture Notes in Computer Science. 5751, pp. 159-179. https://doi.org/10.1007/978-3-642-04167-9_9

A framework for reasoning on component composition

Henrio, L., Kammueller, F. and Khan, M. 2010. A framework for reasoning on component composition. Lecture Notes in Computer Science. 6286, pp. 1-20. https://doi.org/10.1007/978-3-642-17071-3_1

Formalizing non-interference for a simple bytecode language in Coq

Kammueller, F. 2008. Formalizing non-interference for a simple bytecode language in Coq. Formal Aspects of Computing. 20 (3), pp. 259-275.

Mechanical analysis of finite idempotent relations

Kammueller, F. 2011. Mechanical analysis of finite idempotent relations. Fundamenta Informaticae. 107 (1), pp. 43-65. https://doi.org/10.3233/FI-2011-392

Privacy enforcement and analysis for functional active objects

Kammueller, F. 2011. Privacy enforcement and analysis for functional active objects. Lecture Notes in Computer Science. 6514, pp. 93-107. https://doi.org/10.1007/978-3-642-19348-4_8

Bandwidth prediction based on nu-support vector regression and parallel hybrid particle swarm optimization

Cheng, X., Che, X. and Hu, L. 2010. Bandwidth prediction based on nu-support vector regression and parallel hybrid particle swarm optimization. International Journal of Computational Intelligence Systems. 3 (1), pp. 70-83. https://doi.org/10.2991/ijcis.2010.3.1.7

Resource discovery using mobile agents

Singh, M., Cheng, X. and Belavkin, R. 2010. Resource discovery using mobile agents. Frontier of Computer Science and Technology (FCST), 2010 Fifth International Conference. Changchun, Jilin Province 18 - 22 Aug 2010 IEEE. pp. 72 -77 https://doi.org/10.1109/FCST.2010.93

Resource discovery using mobile agents

Singh, M., Cheng, X. and He, X. 2009. Resource discovery using mobile agents. in: Tao, D., Xu, D. and Li, X. (ed.) Semantic Mining Technologies for Multimedia Databases. New York, USA Information Science Reference. pp. 419-448

New e-Learning system architecture based on knowledge engineering technology

Li, Y., Chen, Z., Huang, R. and Cheng, X. 2009. New e-Learning system architecture based on knowledge engineering technology. 2009 IEEE International Conference on Systems, Man and Cybernetics. San Antonio, TX, USA 11 - 14 Oct 2009 IEEE. pp. 5140-5144 https://doi.org/10.1109/ICSMC.2009.5346013

Ubiquitous e-learning System for dynamic mini-courseware assembling and delivering to mobile terminals

Li, Y., Guo, H., Gao, G., Huang, R. and Cheng, X. 2009. Ubiquitous e-learning System for dynamic mini-courseware assembling and delivering to mobile terminals. in: Kim, J., Delen, D., Jinsoo, P., Ko, F., Rui, C., Hyung, J., Lee, W. and Kou, G. (ed.) NCM 2009: Fifth International Joint Conference on INC, IMS, and IDC; [proceedings]. IEEE. pp. 1081-1086