Visible to the public Biblio

Found 10955 results

Filters: Keyword is pubcrawl  [Clear All Filters]
2021-10-12
Suharsono, Teguh Nurhadi, Anggraini, Dini, Kuspriyanto, Rahardjo, Budi, Gunawan.  2020.  Implementation of Simple Verifiability Metric to Measure the Degree of Verifiability of E-Voting Protocol. 2020 14th International Conference on Telecommunication Systems, Services, and Applications (TSSA. :1–3.
Verifiability is one of the parameters in e-voting that can increase confidence in voting technology with several parties ensuring that voters do not change their votes. Voting has become an important part of the democratization system, both to make choices regarding policies, to elect representatives to sit in the representative assembly, and to elect leaders. the more voters and the wider the distribution, the more complex the social life, and the need to manage the voting process efficiently and determine the results more quickly, electronic-based voting (e-Voting) is becoming a more promising option. The level of confidence in voting depends on the capabilities of the system. E-voting must have parameters that can be used as guidelines, which include the following: Accuracy, Invulnerability, Privacy and Verifiability. The implementation of the simple verifiability metric to measure the degree of verifiability in the e-voting protocol, the researchers can calculate the degree of verifiability in the e-voting protocol and the researchers have been able to assess the proposed e-voting protocol with the standard of the best degree of verifiability is 1, where the value of 1 is is absolutely verified protocol.
Uy, Francis Aldrine A., Vea, Larry A., Binag, Matthew G., Diaz, Keith Anshilo L., Gallardo, Roy G., Navarro, Kevin Jorge A., Pulido, Maria Teresa R., Pinca, Ryan Christopher B., Rejuso, Billy John Rudolfh I., Santos, Carissa Jane R..  2020.  The Potential of New Data Sources in a Data-Driven Transportation, Operation, Management and Assessment System (TOMAS). 2020 IEEE Conference on Technologies for Sustainability (SusTech). :1–8.
We present our journey in constructing the first integrated data warehouse for Philippine transportation research in the hopes of developing a Transportation Decision Support System for impact studies and policy making. We share how we collected data from diverse sources, processed them into a homogeneous format and applied them to our multimodal platform. We also list the challenges we encountered, including bureaucratic delays, data privacy concerns, lack of software, and overlapping datasets. The data warehouse shall serve as a public resource for researchers and professionals, and for government officials to make better-informed policies. The warehouse will also function within our multi-modal platform for measurement, modelling, and visualization of road transportation. This work is our contribution to improve the transportation situation in the Philippines, both in the local and national levels, to boost our economy and overall quality of life.
Jayabalan, Manoj.  2020.  Towards an Approach of Risk Analysis in Access Control. 2020 13th International Conference on Developments in eSystems Engineering (DeSE). :287–292.
Information security provides a set of mechanisms to be implemented in the organisation to protect the disclosure of data to the unauthorised person. Access control is the primary security component that allows the user to authorise the consumption of resources and data based on the predefined permissions. However, the access rules are static in nature, which does not adapt to the dynamic environment includes but not limited to healthcare, cloud computing, IoT, National Security and Intelligence Arena and multi-centric system. There is a need for an additional countermeasure in access decision that can adapt to those working conditions to assess the threats and to ensure privacy and security are maintained. Risk analysis is an act of measuring the threats to the system through various means such as, analysing the user behaviour, evaluating the user trust, and security policies. It is a modular component that can be integrated into the existing access control to predict the risk. This study presents the different techniques and approaches applied for risk analysis in access control. Based on the insights gained, this paper formulates the taxonomy of risk analysis and properties that will allow researchers to focus on areas that need to be improved and new features that could be beneficial to stakeholders.
Yang, Howard H., Arafa, Ahmed, Quek, Tony Q. S., Vincent Poor, H..  2020.  Age-Based Scheduling Policy for Federated Learning in Mobile Edge Networks. ICASSP 2020 - 2020 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). :8743–8747.
Federated learning (FL) is a machine learning model that preserves data privacy in the training process. Specifically, FL brings the model directly to the user equipments (UEs) for local training, where an edge server periodically collects the trained parameters to produce an improved model and sends it back to the UEs. However, since communication usually occurs through a limited spectrum, only a portion of the UEs can update their parameters upon each global aggregation. As such, new scheduling algorithms have to be engineered to facilitate the full implementation of FL. In this paper, based on a metric termed the age of update (AoU), we propose a scheduling policy by jointly accounting for the staleness of the received parameters and the instantaneous channel qualities to improve the running efficiency of FL. The proposed algorithm has low complexity and its effectiveness is demonstrated by Monte Carlo simulations.
Adibi, Mahya, van der Woude, Jacob.  2020.  Distributed Learning Control for Economic Power Dispatch: A Privacy Preserved Approach*. 2020 IEEE 29th International Symposium on Industrial Electronics (ISIE). :821–826.
We present a privacy-preserving distributed reinforcement learning-based control scheme to address the problem of frequency control and economic dispatch in power generation systems. The proposed control approach requires neither a priori system model knowledge nor the mathematical formulation of the generation cost functions. Due to not requiring the generation cost models, the control scheme is capable of dealing with scenarios in which the cost functions are hard to formulate and/or non-convex. Furthermore, it is privacy-preserving, i.e. none of the units in the network needs to communicate its cost function and/or control policy to its neighbors. To realize this, we propose an actor-critic algorithm with function approximation in which the actor step is performed individually by each unit with no need to infer the policies of others. Moreover, in the critic step each generation unit shares its estimate of the local measurements and the estimate of its cost function with the neighbors, and via performing a consensus algorithm, a consensual estimate is achieved. The performance of our proposed control scheme, in terms of minimizing the overall cost while persistently fulfilling the demand and fast reaction and convergence of our distributed algorithm, is demonstrated on a benchmark case study.
Sethi, Kamalakanta, Pradhan, Ankit, Bera, Padmalochan.  2020.  Attribute-Based Data Security with Obfuscated Access Policy for Smart Grid Applications. 2020 International Conference on COMmunication Systems NETworkS (COMSNETS). :503–506.
Smart grid employs intelligent transmission and distribution networks for effective and reliable delivery of electricity. It uses fine-grained electrical measurements to attain optimized reliability and stability by sharing these measurements among different entities of energy management systems of the grid. There are many stakeholders like users, phasor measurement units (PMU), and other entities, with changing requirements involved in the sharing of the data. Therefore, data security plays a vital role in the correct functioning of a power grid network. In this paper, we propose an attribute-based encryption (ABE) for secure data sharing in Smart Grid architectures as ABE enables efficient and secure access control. Also, the access policy is obfuscated to preserve privacy. We use Linear Secret Sharing (LSS) Scheme for supporting any monotone access structures, thereby enhancing the expressiveness of access policies. Finally, we also analyze the security, access policy privacy and collusion resistance properties along with efficiency analysis of our cryptosystem.
Ferraro, Angelo.  2020.  When AI Gossips. 2020 IEEE International Symposium on Technology and Society (ISTAS). :69–71.
The concept of AI Gossip is presented. It is analogous to the traditional understanding of a pernicious human failing. It is made more egregious by the technology of AI, internet, current privacy policies, and practices. The recognition by the technological community of its complacency is critical to realizing its damaging influence on human rights. A current example from the medical field is provided to facilitate the discussion and illustrate the seriousness of AI Gossip. Further study and model development is encouraged to support and facilitate the need to develop standards to address the implications and consequences to human rights and dignity.
Dawit, Nahom Aron, Mathew, Sujith Samuel, Hayawi, Kadhim.  2020.  Suitability of Blockchain for Collaborative Intrusion Detection Systems. 2020 12th Annual Undergraduate Research Conference on Applied Computing (URC). :1–6.
Cyber-security is indispensable as malicious incidents are ubiquitous on the Internet. Intrusion Detection Systems have an important role in detecting and thwarting cyber-attacks. However, it is more effective in a centralized system but not in peer-to-peer networks which makes it subject to central point failure, especially in collaborated intrusion detection systems. The novel blockchain technology assures a fully distributed security system through its powerful features of transparency, immutability, decentralization, and provenance. Therefore, in this paper, we investigate and demonstrate several methods of collaborative intrusion detection with blockchain to analyze the suitability and security of blockchain for collaborative intrusion detection systems. We also studied the difference between the existing means of the integration of intrusion detection systems with blockchain and categorized the major vulnerabilities of blockchain with their potential losses and current enhancements for mitigation.
Sun, Yuxin, Zhang, Yingzhou, Zhu, Linlin.  2020.  An Anti-Collusion Fingerprinting based on CFF Code and RS Code. 2020 International Conference on Cyber-Enabled Distributed Computing and Knowledge Discovery (CyberC). :56–63.
Data security is becoming more and more important in data exchange. Once the data is leaked, it will pose a great threat to the privacy and property security of users. Copyright authentication and data provenance have become an important requirement of the information security defense mechanism. In order to solve the collusion leakage of the data distributed by organization and the low efficiency of tracking the leak provenance after the data is destroyed, this paper proposes a concatenated-group digital fingerprint coding based on CFF code and Reed-solomon (RS) that can resist collusion attacks and corresponding detection algorithm. The experiments based on an asymmetric anti-collusion fingerprint protocol show that the proposed method has better performance to resist collusion attacks than similar non-grouped fingerprint coding and effectively reduces the percentage of misjudgment, which verifies the availability of the algorithm and enriches the means of organization data security audit.
Henry, Wayne C., Peterson, Gilbert L..  2020.  Exploring Provenance Needs in Software Reverse Engineering. 2020 13th International Conference on Systematic Approaches to Digital Forensic Engineering (SADFE). :57–65.
Reverse engineers are in high demand in digital forensics for their ability to investigate malicious cyberspace threats. This group faces unique challenges due to the security-intensive environment, such as working in isolated networks, a limited ability to share files with others, immense time pressure, and a lack of cognitive support tools supporting the iterative exploration of binary executables. This paper presents an exploratory study that interviewed experienced reverse engineers' work processes, tools, challenges, and visualization needs. The findings demonstrate that engineers have difficulties managing hypotheses, organizing results, and reporting findings during their analysis. By considering the provenance support techniques of existing research in other domains, this study contributes new insights about the needs and opportunities for reverse engineering provenance tools.
Hassan, Wajih Ul, Bates, Adam, Marino, Daniel.  2020.  Tactical Provenance Analysis for Endpoint Detection and Response Systems. 2020 IEEE Symposium on Security and Privacy (SP). :1172–1189.
Endpoint Detection and Response (EDR) tools provide visibility into sophisticated intrusions by matching system events against known adversarial behaviors. However, current solutions suffer from three challenges: 1) EDR tools generate a high volume of false alarms, creating backlogs of investigation tasks for analysts; 2) determining the veracity of these threat alerts requires tedious manual labor due to the overwhelming amount of low-level system logs, creating a "needle-in-a-haystack" problem; and 3) due to the tremendous resource burden of log retention, in practice the system logs describing long-lived attack campaigns are often deleted before an investigation is ever initiated.This paper describes an effort to bring the benefits of data provenance to commercial EDR tools. We introduce the notion of Tactical Provenance Graphs (TPGs) that, rather than encoding low-level system event dependencies, reason about causal dependencies between EDR-generated threat alerts. TPGs provide compact visualization of multi-stage attacks to analysts, accelerating investigation. To address EDR's false alarm problem, we introduce a threat scoring methodology that assesses risk based on the temporal ordering between individual threat alerts present in the TPG. In contrast to the retention of unwieldy system logs, we maintain a minimally-sufficient skeleton graph that can provide linkability between existing and future threat alerts. We evaluate our system, RapSheet, using the Symantec EDR tool in an enterprise environment. Results show that our approach can rank truly malicious TPGs higher than false alarm TPGs. Moreover, our skeleton graph reduces the long-term burden of log retention by up to 87%.
Sharma, Rohit, Pawar, Siddhesh, Gurav, Siddhita, Bhavathankar, Prasenjit.  2020.  A Unique Approach towards Image Publication and Provenance using Blockchain. 2020 Third International Conference on Smart Systems and Inventive Technology (ICSSIT). :311–314.
The recent spurt of incidents related to copyrights and security breaches has led to the monetary loss of several digital content creators and publishers. These incidents conclude that the existing system lacks the ability to uphold the integrity of their published content. Moreover, some of the digital content owners rely on third parties, results in lack of ability to provide provenance of digital media. The question that needs to be addressed today is whether modern technologies can be leveraged to suppress such incidents and regain the confidence of creators and the audience. Fortunately, this paper presents a unique framework that empowers digital content creators to have complete control over the place of its origin, accessibility and impose restrictions on unauthorized alteration of their content. This framework harnesses the power of the Ethereum platform, a part of Blockchain technology, and uses S mart Contracts as a key component empowering the creators with enhanced control of their content and the corresponding audience.
Kashliev, Andrii.  2020.  Storage and Querying of Large Provenance Graphs Using NoSQL DSE. 2020 IEEE 6th Intl Conference on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on Intelligent Data and Security (IDS). :260–262.
Provenance metadata captures history of derivation of an entity, such as a dataset obtained through numerous data transformations. It is of great importance for science, among other fields, as it enables reproducibility and greater intelligibility of research results. With the avalanche of provenance produced by today's society, there is a pressing need for storing and low-latency querying of large provenance graphs. To address this need, in this paper we present a scalable approach to storing and querying provenance graphs using a popular NoSQL column family database system called DataStax Enterprise (DSE). Specifically, we i) propose a storage scheme, including two novel indices that enable efficient traversal of provenance graphs along causality lines, ii) present an algorithm for building our proposed indices for a given provenance graph, iii) implement our algorithm and conduct a performance study in which we store and query a provenance graph with over five million vertices using a DSE cluster running in AWS cloud. Our performance study results further validate scalability and performance efficiency of our approach.
Gouk, Henry, Hospedales, Timothy M..  2020.  Optimising Network Architectures for Provable Adversarial Robustness. 2020 Sensor Signal Processing for Defence Conference (SSPD). :1–5.
Existing Lipschitz-based provable defences to adversarial examples only cover the L2 threat model. We introduce the first bound that makes use of Lipschitz continuity to provide a more general guarantee for threat models based on any Lp norm. Additionally, a new strategy is proposed for designing network architectures that exhibit superior provable adversarial robustness over conventional convolutional neural networks. Experiments are conducted to validate our theoretical contributions, show that the assumptions made during the design of our novel architecture hold in practice, and quantify the empirical robustness of several Lipschitz-based adversarial defence methods.
Dong, Sichen, Jiao, Jian, Li, Shuyu.  2020.  A Multiple-Replica Provable Data Possession Algorithm Based on Branch Authentication Tree. 2020 IEEE 11th International Conference on Software Engineering and Service Science (ICSESS). :400–404.
The following topics are dealt with: learning (artificial intelligence); neural nets; feature extraction; pattern classification; convolutional neural nets; computer network security; security of data; recurrent neural nets; data privacy; and cloud computing.
Muller, Tim, Wang, Dongxia, Sun, Jun.  2020.  Provably Robust Decisions based on Potentially Malicious Sources of Information. 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). :411–424.
Sometimes a security-critical decision must be made using information provided by peers. Think of routing messages, user reports, sensor data, navigational information, blockchain updates. Attackers manifest as peers that strategically report fake information. Trust models use the provided information, and attempt to suggest the correct decision. A model that appears accurate by empirical evaluation of attacks may still be susceptible to manipulation. For a security-critical decision, it is important to take the entire attack space into account. Therefore, we define the property of robustness: the probability of deciding correctly, regardless of what information attackers provide. We introduce the notion of realisations of honesty, which allow us to bypass reasoning about specific feedback. We present two schemes that are optimally robust under the right assumptions. The “majority-rule” principle is a special case of the other scheme which is more general, named “most plausible realisations”.
El-Sobky, Mariam, Sarhan, Hisham, Abu-ElKheir, Mervat.  2020.  Security Assessment of the Contextual Multi-Armed Bandit - RL Algorithm for Link Adaptation. 2020 2nd Novel Intelligent and Leading Emerging Sciences Conference (NILES). :514–519.
Industry is increasingly adopting Reinforcement Learning algorithms (RL) in production without thoroughly analyzing their security features. In addition to the potential threats that may arise if the functionality of these algorithms is compromised while in operation. One of the well-known RL algorithms is the Contextual Multi-Armed Bandit (CMAB) algorithm. In this paper, we explore how the CMAB can be used to solve the Link Adaptation problem - a well-known problem in the telecommunication industry by learning the optimal transmission parameters that will maximize a communication link's throughput. We analyze the potential vulnerabilities of the algorithm and how they may adversely affect link parameters computation. Additionally, we present a provable security assessment for the Contextual Multi-Armed Bandit Reinforcement Learning (CMAB-RL) algorithm in a network simulated environment using Ray. This is by demonstrating CMAB security vulnerabilities theoretically and practically. Some security controls are proposed for CMAB agent and the surrounding environment. In order to fix those vulnerabilities and mitigate the risk. These controls can be applied to other RL agents in order to design more robust and secure RL agents.
Li, Xinyu, Xu, Jing, Zhang, Zhenfeng, Lan, Xiao, Wang, Yuchen.  2020.  Modular Security Analysis of OAuth 2.0 in the Three-Party Setting. 2020 IEEE European Symposium on Security and Privacy (EuroS P). :276–293.
OAuth 2.0 is one of the most widely used Internet protocols for authorization/single sign-on (SSO) and is also the foundation of the new SSO protocol OpenID Connect. Due to its complexity and its flexibility, it is difficult to comprehensively analyze the security of the OAuth 2.0 standard, yet it is critical to obtain practical security guarantees for OAuth 2.0. In this paper, we present the first computationally sound security analysis of OAuth 2.0. First, we introduce a new primitive, the three-party authenticated secret distribution (3P-ASD for short) protocol, which plays the role of issuing the secret and captures the token issue process of OAuth 2.0. As far as we know, this is the first attempt to formally abstract the authorization technology into a general primitive and then define its security. Then, we present a sufficiently rich three-party security model for OAuth protocols, covering all kinds of authorization flows, providing reasonably strong security guarantees and moreover capturing various web features. To confirm the soundness of our model, we also identify the known attacks against OAuth 2.0 in the model. Furthermore, we prove that two main modes of OAuth 2.0 can achieve our desired security by abstracting the token issue process into a 3P-ASD protocol. Our analysis is not only modular which can reflect the compositional nature of OAuth 2.0, but also fine-grained which can evaluate how the intermediate parameters affect the final security of OAuth 2.0.
Zhou, Yimin, Zhang, Kai.  2020.  DoS Vulnerability Verification of IPSec VPN. 2020 IEEE International Conference on Artificial Intelligence and Computer Applications (ICAICA). :698–702.
This paper analyzes the vulnerability in the process of key negotiation between the main mode and aggressive mode of IKEv1 protocol in IPSec VPN, and proposes a DOS attack method based on OSPF protocol adjacent route spoofing. The experiment verifies the insecurity of IPSec VPN using IKEv1 protocol. This attack method has the advantages of lower cost and easier operation compared with using botnet.
Vinarskii, Evgenii, Demakov, Alexey, Kamkin, Alexander, Yevtushenko, Nina.  2020.  Verifying cryptographic protocols by Tamarin Prover. 2020 Ivannikov Memorial Workshop (IVMEM). :69–75.
Cryptographic protocols are utilized for establishing a secure session between “honest” agents which communicate strictly according to the protocol rules as well as for ensuring the authenticated and confidential transmission of messages. The specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages including the format of such messages. Note that protocol can describe several execution scenarios. All these requirements lead to a huge formal specification for a real cryptographic protocol and therefore, it is difficult to verify the security of the whole cryptographic protocol at once. In this paper, to overcome this problem, we suggest verifying the protocol security for its fragments. Namely, we verify the security properties for a special set of so-called traces of the cryptographic protocol. Intuitively, a trace of the cryptographic protocol is a sequence of computations, value checks, and transmissions on the sides of “honest” agents permitted by the protocol. In order to choose such set of traces, we introduce an Adversary model and the notion of a similarity relation for traces. We then verify the security properties of selected traces with Tamarin Prover. Experimental results for the EAP and Noise protocols clearly show that this approach can be promising for automatic verification of large protocols.
Hassan, Mehmood, Sultan, Aiman, Awan, Ali Afzal, Tahir, Shahzaib, Ihsan, Imran.  2020.  An Enhanced and Secure Multiserver-based User Authentication Protocol. 2020 International Conference on Cyber Warfare and Security (ICCWS). :1–6.
The extensive use of the internet and web-based applications spot the multiserver authentication as a significant component. The users can get their services after authenticating with the service provider by using similar registration records. Various protocol schemes are developed for multiserver authentication, but the existing schemes are not secure and often lead towards various vulnerabilities and different security issues. Recently, Zhao et al. put forward a proposal for smart card and user's password-based authentication protocol for the multiserver environment and showed that their proposed protocol is efficient and secure against various security attacks. This paper points out that Zhao et al.'s authentication scheme is susceptive to traceability as well as anonymity attacks. Thus, it is not feasible for the multiserver environment. Furthermore, in their scheme, it is observed that a user while authenticating does not send any information with any mention of specific server identity. Therefore, this paper proposes an enhanced, efficient and secure user authentication scheme for use in any multiserver environment. The formal security analysis and verification of the protocol is performed using state-of-the-art tool “ProVerif” yielding that the proposed scheme provides higher levels of security.
Kai, Wang, Wei, Li, Tao, Chen, Longmei, Nan.  2020.  Research on Secure JTAG Debugging Model Based on Schnorr Identity Authentication Protocol. 2020 IEEE 15th International Conference on Solid-State Integrated Circuit Technology (ICSICT). :1–3.
As a general interface for chip system testing and on-chip debugging, JTAG is facing serious security threats. By analyzing the typical JTAG attack model and security protection measures, this paper designs a secure JTAG debugging model based on Schnorr identity authentication protocol, and takes RISCV as an example to build a set of SoC prototype system to complete functional verification. Experiments show that this secure JTAG debugging model has high security, flexible implementation, and good portability. It can meet the JTAG security protection requirements in various application scenarios. The maximum clock frequency can reach 833MHZ, while the hardware overhead is only 47.93KGate.
Li, Yongjian, Cao, Taifeng, Jansen, David N., Pang, Jun, Wei, Xiaotao.  2020.  Accelerated Verification of Parametric Protocols with Decision Trees. 2020 IEEE 38th International Conference on Computer Design (ICCD). :397–404.
Within a framework for verifying parametric network protocols through induction, one needs to find invariants based on a protocol instance of a small number of nodes. In this paper, we propose a new approach to accelerate parameterized verification by adopting decision trees to represent the state space of a protocol instance. Such trees can be considered as a knowledge base that summarizes all behaviors of the protocol instance. With this knowledge base, we are able to efficiently construct an oracle to effectively assess candidates of invariants of the protocol, which are suggested by an invariant finder. With the discovered invariants, a formal proof for the correctness of the protocol can be derived in the framework after proper generalization. The effectiveness of our method is demonstrated by experiments with typical benchmarks.
He, Leifeng, Liu, Guanjun.  2020.  Petri Nets Based Verification of Epistemic Logic and Its Application on Protocols of Privacy and Security. 2020 IEEE World Congress on Services (SERVICES). :25–28.
Epistemic logic can specify many design requirements of privacy and security of multi-agent systems (MAS). The existing model checkers of epistemic logic use some programming languages to describe MAS, induce Kripke models as the behavioral representation of MAS, apply Ordered Binary Decision Diagrams (OBDD) to encode Kripke models to solve their state explosion problem and verify epistemic logic based on the encoded Kripke models. However, these programming languages are usually non-intuitive. More seriously, their OBDD-based model checking processes are often time-consuming due to their dynamic variable ordering for OBDD. Therefore, we define Knowledge-oriented Petri Nets (KPN) to intuitively describe MAS, induce similar reachability graphs as the behavioral representation of KPN, apply OBDD to encode all reachable states, and finally verify epistemic logic. Although we also use OBDD, we adopt a heuristic method for the computation of a static variable order instead of dynamic variable ordering. More importantly, while verifying an epistemic formula, we dynamically generate its needed similar relations, which makes our model checking process much more efficient. In this paper, we introduce our work.
Remlein, Piotr, Rogacki, Mikołaj, Stachowiak, Urszula.  2020.  Tamarin software – the tool for protocols verification security. 2020 Baltic URSI Symposium (URSI). :118–123.
In order to develop safety-reliable standards for IoT (Internet of Things) networks, appropriate tools for their verification are needed. Among them there is a group of tools based on automated symbolic analysis. Such a tool is Tamarin software. Its usage for creating formal proofs of security protocols correctness has been presented in this paper using the simple example of an exchange of messages with asynchronous encryption between two agents. This model can be used in sensor networks or IoT e.g. in TLS protocol to provide a mechanism for secure cryptographic key exchange.