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
TypeConference paper
TitleDNSsec in Isabelle – replay attack and origin authentication
AuthorsKammueller, 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.

KeywordsDNSsec; Isabelle/HOL; authentication; replay attack
LanguageEnglish
ConferenceSMC 2013: IEEE International Conference on Systems, Man, and Cybernetics
Page range4772-4777
Proceedings Title2013 IEEE International Conference on Systems, Man, and Cybernetics
SeriesIEEE International Conference on Systems Man and Cybernetics Conference Proceedings
ISSN1062-922X
ISBN
Electronic9781479906529
PublisherIEEE
Publication dates
Print13 Oct 2013
Print27 Jan 2014
Publication process dates
Deposited23 Apr 2015
Output statusPublished
Digital Object Identifier (DOI)https://doi.org/10.1109/SMC.2013.812
Web of Science identifierWOS:000332201904155
Web address (URL) of conference proceedingshttps://ieeexplore.ieee.org/xpl/conhome/6689802/proceeding
Permalink -

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

Log in to edit
  • 41
    total views
  • 0
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as

Related outputs

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
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
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
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
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
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. Human Computer Interaction International. Virtual 26 Jun - 01 Jul 2022
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
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
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
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
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
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
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
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
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
A formal development cycle for security engineering in Isabelle
Kammueller, F. 2020. A formal development cycle for security engineering in Isabelle. arxiv.org.
Applying the Isabelle Insider framework to airplane security
Kammueller, F. and Kerber, M. 2020. Applying the Isabelle Insider framework to airplane security. arxiv.org.
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
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
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 LIPICS --Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany. pp. 11:1-11:12 https://doi.org/10.4230/OASIcs.FMBC.2020.11
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
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
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
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
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
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
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
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
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.
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
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
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. https://doi.org/10.1142/s0218348x17400047
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
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).
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
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
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
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
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
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
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
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
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.
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
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
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
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
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
Resource discovery using mobile agents [book section]
Singh, M., Cheng, X. and He, X. 2009. Resource discovery using mobile agents [book section]. in: Tao, D., Xu, D. and Li, X. (ed.) Semantic Mining Technologies for Multimedia Databases. New York, USA Information Science Reference. pp. 419-448
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).
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. Systems, Man and Cybernetics, IEEE International Conference. 2009.
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 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
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
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
Formal verification of the merchant registration phase of the SET protocol.
Cheng, X. and Ma, X. 2005. Formal verification of the merchant registration phase of the SET protocol. International Journal of Automation and Computing. 2 (2), pp. 155-162. https://doi.org/10.1007/s11633-005-0155-5
Programming style based program partition
Li, Y., Yang, H., Cheng, X. and Zhu, X. 2005. Programming style based program partition. International Journal of Software Engineering and Knowledge Engineering. 15 (6), pp. 1027-1062. https://doi.org/10.1142/S0218194005002610
An improved model-based method to test circuit faults
Cheng, X., Ouyang, D., Yunfei, J. and Zhang, C. 2005. An improved model-based method to test circuit faults. Theoretical Computer Science. 341 (1-3), pp. 150-161. https://doi.org/10.1016/j.tcs.2005.04.004
Topology control of ad hoc wireless networks for energy efficiency
Cheng, M., Cardei, M., Sun, J., Cheng, X., Wang, L., Xu, Y. and Du, D. 2004. Topology control of ad hoc wireless networks for energy efficiency. IEEE Transactions on Computers. 53 (12), pp. 1629-1635. https://doi.org/10.1109/TC.2004.121