Visible to the public Biblio

Found 1422 results

Filters: First Letter Of Title is A  [Clear All Filters]
[A] B C D E F G H I J K L M N O P Q R S T U V W X Y Z   [Show ALL]
A
Ghazo, A. T. Al, Ibrahim, M., Ren, H., Kumar, R..  2020.  A2G2V: Automatic Attack Graph Generation and Visualization and Its Applications to Computer and SCADA Networks. IEEE Transactions on Systems, Man, and Cybernetics: Systems. 50:3488–3498.
Securing cyber-physical systems (CPS) and Internet of Things (IoT) systems requires the identification of how interdependence among existing atomic vulnerabilities may be exploited by an adversary to stitch together an attack that can compromise the system. Therefore, accurate attack graphs play a significant role in systems security. A manual construction of the attack graphs is tedious and error-prone, this paper proposes a model-checking-based automated attack graph generator and visualizer (A2G2V). The proposed A2G2V algorithm uses existing model-checking tools, an architecture description tool, and our own code to generate an attack graph that enumerates the set of all possible sequences in which atomic-level vulnerabilities can be exploited to compromise system security. The architecture description tool captures a formal representation of the networked system, its atomic vulnerabilities, their pre-and post-conditions, and security property of interest. A model-checker is employed to automatically identify an attack sequence in the form of a counterexample. Our own code integrated with the model-checker parses the counterexamples, encodes those for specification relaxation, and iterates until all attack sequences are revealed. Finally, a visualization tool has also been incorporated with A2G2V to generate a graphical representation of the generated attack graph. The results are illustrated through application to computer as well as control (SCADA) networks.
Tairi, Erkan, Moreno-Sanchez, Pedro, Maffei, Matteo.  2021.  A2L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs. 2021 IEEE Symposium on Security and Privacy (SP). :1834–1851.
Payment channel hubs (PCHs) constitute a promising solution to the inherent scalability problem of blockchain technologies, allowing for off-chain payments between sender and receiver through an intermediary, called the tumbler. While state-of-the-art PCHs provide security and privacy guarantees against a malicious tumbler, they do so by relying on the scripting-based functionality available only at few cryptocurrencies, and they thus fall short of fundamental properties such as backwards compatibility and efficiency.In this work, we present the first PCH protocol to achieve all aforementioned properties. Our PCH builds upon A2L, a novel cryptographic primitive that realizes a three-party protocol for conditional transactions, where the tumbler pays the receiver only if the latter solves a cryptographic challenge with the help of the sender, which implies the sender has paid the tumbler. We prove the security and privacy guarantees of A2L (which carry over to our PCH construction) in the Universal Composability framework and present a provably secure instantiation based on adaptor signatures and randomizable puzzles. We implemented A2L and compared it to TumbleBit, the state-of-the-art Bitcoin-compatible PCH. Asymptotically, A2L has a communication complexity that is constant, as opposed to linear in the security parameter like in TumbleBit. In practice, A2L requires 33x less bandwidth than TumleBit, while retaining the computational cost (or providing 2x speedup with a preprocessing technique). This demonstrates that A2L (and thus our PCH construction) is ready to be deployed today.In theory, we demonstrate for the first time that it is possible to design a secure and privacy-preserving PCH while requiring only digital signatures and timelock functionality from the underlying scripting language. In practice, this result makes our PCH backwards compatible with virtually all cryptocurrencies available today, even those offering a highly restricted form of scripting language such as Ripple or Stellar. The practical appealing of our construction has resulted in a proof-of-concept implementation in the COMIT Network, a blockchain technology focused on cross-currency payments.
Mohandas, Nair Arun, Swathi, Adinath, R., Abhijith, Nazar, Ajmal, Sharath, Greeshma.  2020.  A4: A Lightweight Stream Cipher. 2020 5th International Conference on Communication and Electronics Systems (ICCES). :573—577.
Lightweight ciphers are algorithms with low computational and spacial complexity. In the modern world of miniaturization, a lightweight cipher is used in constrained devices such as RFID tags, fire and security detectors, devices for wireless communications and other IoT devices. Stream ciphers are symmetric ciphers which encrypts the plain text bit stream with corresponding key stream to generate cipher text. Hence a stream cipher with low computational complexity and maximum security can be termed as a lightweight stream cipher. Many light weight stream ciphers are already existing. Each has its own vulnerabilities and spacial requirement. This paper has successfully developed, implemented, and analyzed a lightweight stream cipher - A4. Along with low computational cost, A4 also ensures paramount security and is less prone to the emerging cryptographic attacks.
Hossen, Imran, Hei, Xiali.  2022.  aaeCAPTCHA: The Design and Implementation of Audio Adversarial CAPTCHA. 2022 IEEE 7th European Symposium on Security and Privacy (EuroS&P). :430–447.
CAPTCHAs are designed to prevent malicious bot programs from abusing websites. Most online service providers deploy audio CAPTCHAs as an alternative to text and image CAPTCHAs for visually impaired users. However, prior research investigating the security of audio CAPTCHAs found them highly vulnerable to automated attacks using Automatic Speech Recognition (ASR) systems. To improve the robustness of audio CAPTCHAs against automated abuses, we present the design and implementation of an audio adversarial CAPTCHA (aaeCAPTCHA) system in this paper. The aaeCAPTCHA system exploits audio adversarial examples as CAPTCHAs to prevent the ASR systems from automatically solving them. Furthermore, we conducted a rigorous security evaluation of our new audio CAPTCHA design against five state-of-the-art DNN-based ASR systems and three commercial Speech-to-Text (STT) services. Our experimental evaluations demonstrate that aaeCAPTCHA is highly secure against these speech recognition technologies, even when the attacker has complete knowledge of the current attacks against audio adversarial examples. We also conducted a usability evaluation of the proof-of-concept implementation of the aaeCAPTCHA scheme. Our results show that it achieves high robustness at a moderate usability cost compared to normal audio CAPTCHAs. Finally, our extensive analysis highlights that aaeCAPTCHA can significantly enhance the security and robustness of traditional audio CAPTCHA systems while maintaining similar usability.
Wei Liu, Ming Yu.  2014.  AASR: Authenticated Anonymous Secure Routing for MANETs in Adversarial Environments. Vehicular Technology, IEEE Transactions on. 63:4585-4593.

Anonymous communications are important for many of the applications of mobile ad hoc networks (MANETs) deployed in adversary environments. A major requirement on the network is the ability to provide unidentifiability and unlinkability for mobile nodes and their traffic. Although a number of anonymous secure routing protocols have been proposed, the requirement is not fully satisfied. The existing protocols are vulnerable to the attacks of fake routing packets or denial-of-service broadcasting, even the node identities are protected by pseudonyms. In this paper, we propose a new routing protocol, i.e., authenticated anonymous secure routing (AASR), to satisfy the requirement and defend against the attacks. More specifically, the route request packets are authenticated by a group signature, to defend against potential active attacks without unveiling the node identities. The key-encrypted onion routing with a route secret verification message is designed to prevent intermediate nodes from inferring a real destination. Simulation results have demonstrated the effectiveness of the proposed AASR protocol with improved performance as compared with the existing protocols.

Bhatt, Smriti, Patwa, Farhan, Sandhu, Ravi.  2017.  ABAC with Group Attributes and Attribute Hierarchies Utilizing the Policy Machine. Proceedings of the 2Nd ACM Workshop on Attribute-Based Access Control. :17–28.

Attribute-Based Access Control (ABAC) has received significant attention in recent years, although the concept has been around for over two decades now. Many ABAC models, with different variations, have been proposed and formalized. Besides basic ABAC models, there are models designed with additional capabilities such as group attributes, group and attribute hierarchies and so on. Hierarchical relationship among groups and attributes enhances access control flexibility and facilitates attribute management and administration. However, implementation and demonstration of ABAC models in real-world applications is still lacking. In this paper, we present a restricted HGABAC (rHGABAC) model with user and object groups and group hierarchy. We then introduce attribute hierarchies in this model. We also present an authorization architecture for implementing rHGABAC utilizing the NIST Policy Machine (PM). PM allows to define attribute-based access control policies, however, the attributes in PM are different in nature than attributes in typical ABAC models as name-value pairs. We identify a policy configuration mechanism for our proposed model employing PM capabilities, and demonstrate use cases and their configuration and implementation in PM using our authorization architecture.

Gorbenko, A., Popov, V..  2020.  Abnormal Behavioral Pattern Detection in Closed-Loop Robotic Systems for Zero-Day Deceptive Threats. 2020 International Conference on Industrial Engineering, Applications and Manufacturing (ICIEAM). :1—6.

In recent years, attacks against cyber-physical systems have become increasingly frequent and widespread. The inventiveness of such attacks increases significantly. In particular, zero-day attacks are widely used. The rapid development of the industrial Internet of things, the expansion of the application areas of service robots, the advent of the Internet of vehicles and the Internet of military things have led to a significant increase of attention to deceptive attacks. Especially great threat is posed by deceptive attacks that do not use hiding malicious components. Such attacks can naturally be used against robotic systems. In this paper, we consider an approach to the development of an intrusion detection system for closed-loop robotic systems. The system is based on an abnormal behavioral pattern detection technique. The system can be used for detection of zero-day deceptive attacks. We provide an experimental comparison of our approach and other behavior-based intrusion detection systems.

Dong, C., Liu, Y., Zhang, Y., Shi, P., Shao, X., Ma, C..  2018.  Abnormal Bus Data Detection of Intelligent and Connected Vehicle Based on Neural Network. 2018 IEEE International Conference on Computational Science and Engineering (CSE). :171–176.
In the paper, our research of abnormal bus data analysis of intelligent and connected vehicle aims to detect the abnormal data rapidly and accurately generated by the hackers who send malicious commands to attack vehicles through three patterns, including remote non-contact, short-range non-contact and contact. The research routine is as follows: Take the bus data of 10 different brands of intelligent and connected vehicles through the real vehicle experiments as the research foundation, set up the optimized neural network, collect 1000 sets of the normal bus data of 15 kinds of driving scenarios and the other 300 groups covering the abnormal bus data generated by attacking the three systems which are most common in the intelligent and connected vehicles as the training set. In the end after repeated amendments, with 0.5 seconds per detection, the intrusion detection system has been attained in which for the controlling system the abnormal bus data is detected at the accuracy rate of 96% and the normal data is detected at the accuracy rate of 90%, for the body system the abnormal one is 87% and the normal one is 80%, for the entertainment system the abnormal one is 80% and the normal one is 65%.
Yueguo Zhang, Lili Dong, Shenghong Li, Jianhua Li.  2014.  Abnormal crowd behavior detection using interest points. Broadband Multimedia Systems and Broadcasting (BMSB), 2014 IEEE International Symposium on. :1-4.

Abnormal crowd behavior detection is an important research issue in video processing and computer vision. In this paper we introduce a novel method to detect abnormal crowd behaviors in video surveillance based on interest points. A complex network-based algorithm is used to detect interest points and extract the global texture features in scenarios. The performance of the proposed method is evaluated on publicly available datasets. We present a detailed analysis of the characteristics of the crowd behavior in different density crowd scenes. The analysis of crowd behavior features and simulation results are also demonstrated to illustrate the effectiveness of our proposed method.

Shin, Ho-Chul.  2019.  Abnormal Detection based on User Feedback for Abstracted Pedestrian Video. 2019 International Conference on Information and Communication Technology Convergence (ICTC). :1036–1038.
In this study, we present the abstracted pedestrian behavior representation and abnormal detection method based on user feedback for pedestrian video surveillance system. Video surveillance data is large in size and difficult to process in real time. To solve this problem, we suggested a method of expressing the pedestrian behavior with abbreviated map. In the video surveillance system, false detection of an abnormal situation becomes a big problem. If surveillance user can guide the false detection case as human in the loop, the surveillance system can learn the case and reduce the false detection error in the future. We suggested user feedback based abnormal pedestrian detection method. By the suggested user feedback algorithm, the false detection can be reduced to less than 0.5%.
Qi, L. T., Huang, H. P., Wang, P., Wang, R. C..  2018.  Abnormal Item Detection Based on Time Window Merging for Recommender Systems. 2018 17th IEEE International Conference On Trust, Security And Privacy In Computing And Communications/ 12th IEEE International Conference On Big Data Science And Engineering (TrustCom/BigDataSE). :252–259.

CFRS (Collaborative Filtering Recommendation System) is one of the most widely used individualized recommendation systems. However, CFRS is susceptible to shilling attacks based on profile injection. The current research on shilling attack mainly focuses on the recognition of false user profiles, but these methods depend on the specific attack models and the computational cost is huge. From the view of item, some abnormal item detection methods are proposed which are independent of attack models and overcome the defects of user profiles model, but its detection rate, false alarm rate and time overhead need to be further improved. In order to solve these problems, it proposes an abnormal item detection method based on time window merging. This method first uses the small window to partition rating time series, and determine whether the window is suspicious in terms of the number of abnormal ratings within it. Then, the suspicious small windows are merged to form suspicious intervals. We use the rating distribution characteristics RAR (Ratio of Abnormal Rating), ATIAR (Average Time Interval of Abnormal Rating), DAR(Deviation of Abnormal Rating) and DTIAR (Deviation of Time Interval of Abnormal Rating) in the suspicious intervals to determine whether the item is subject to attacks. Experiment results on the MovieLens 100K data set show that the method has a high detection rate and a low false alarm rate.

Shin, Ho-Chul, Na, Kiin.  2021.  Abnormal Situation Detection using Global Surveillance Map. 2021 International Conference on Information and Communication Technology Convergence (ICTC). :769–772.
in this paper, we describe a method for detecting abnormal pedestrians or cars by expressing the behavioral characteristics of pedestrians on a global surveillance map in a video security system using CCTV and patrol robots. This method converts a large amount of video surveillance data into a compressed map shape format to efficiently transmit and process data. By using deep learning auto-encoder and CNN algorithm, pedestrians belonging to the abnormal category can be detected in two steps. In the case of the first-stage abnormal candidate extraction, the normal detection rate was 87.7%, the abnormal detection rate was 88.3%, and in the second stage abnormal candidate filtering, the normal detection rate was 99.8% and the abnormal detection rate was 96.5%.
Liu, X., Gao, W., Feng, D., Gao, X..  2020.  Abnormal Traffic Congestion Recognition Based on Video Analysis. 2020 IEEE Conference on Multimedia Information Processing and Retrieval (MIPR). :39—42.

The incidence of abnormal road traffic events, especially abnormal traffic congestion, is becoming more and more prominent in daily traffic management in China. It has become the main research work of urban traffic management to detect and identify traffic congestion incidents in time. Efficient and accurate detection of traffic congestion incidents can provide a good strategy for traffic management. At present, the detection and recognition of traffic congestion events mainly rely on the integration of road traffic flow data and the passing data collected by electronic police or devices of checkpoint, and then estimating and forecasting road conditions through the method of big data analysis; Such methods often have some disadvantages such as low time-effect, low precision and small prediction range. Therefore, with the help of the current large and medium cities in the public security, traffic police have built video surveillance equipment, through computer vision technology to analyze the traffic flow from video monitoring, in this paper, the motion state and the changing trend of vehicle flow are obtained by using the technology of vehicle detection from video and multi-target tracking based on deep learning, so as to realize the perception and recognition of traffic congestion. The method achieves the recognition accuracy of less than 60 seconds in real-time, more than 80% in detection rate of congestion event and more than 82.5% in accuracy of detection. At the same time, it breaks through the restriction of traditional big data prediction, such as traffic flow data, truck pass data and GPS floating car data, and enlarges the scene and scope of detection.

Le, Van-Khoa, Beauseroy, Pierre, Grall-Maes, Edith.  2018.  Abnormal Trajectory Detection for Security Infrastructure. Proceedings of the 2Nd International Conference on Digital Signal Processing. :1–5.

In this work, an approach for the automatic analysis of people trajectories is presented, using a multi-camera and card reader system. Data is first extracted from surveillance cameras and card readers to create trajectories which are sequences of paths and activities. A distance model is proposed to compare sequences and calculate similarities. The popular unsupervised model One-Class Support Vector Machine (One-Class SVM) is used to train a detector. The proposed method classifies trajectories as normal or abnormal and can be used in two modes: off-line and real-time. Experiments are based on data simulation corresponding to an attack scenario proposed by a security expert. Results show that the proposed method successfully detects the abnormal sequences in the scenario with very low false alarm rate.

Liao, Q., Gu, Y., Liao, J., Li, W..  2020.  Abnormal transaction detection of Bitcoin network based on feature fusion. 2020 IEEE 9th Joint International Information Technology and Artificial Intelligence Conference (ITAIC). 9:542—549.

Anomaly detection is one of the research hotspots in Bitcoin transaction data analysis. In view of the existing research that only considers the transaction as an isolated node when extracting features, but has not yet used the network structure to dig deep into the node information, a bitcoin abnormal transaction detection method that combines the node’s own features and the neighborhood features is proposed. Based on the formation mechanism of the interactive relationship in the transaction network, first of all, according to a certain path selection probability, the features of the neighbohood nodes are extracted by way of random walk, and then the node’s own features and the neighboring features are fused to use the network structure to mine potential node information. Finally, an unsupervised detection algorithm is used to rank the transaction points on the constructed feature set to find abnormal transactions. Experimental results show that, compared with the existing feature extraction methods, feature fusion improves the ability to detect abnormal transactions.

Sharma, Manoj Kumar, Sheet, Debdoot, Biswas, Prabir Kumar.  2016.  Abnormality Detecting Deep Belief Network. Proceedings of the International Conference on Advances in Information Communication Technology & Computing. :11:1–11:6.

Abnormality detection is useful in reducing the amount of data to be processed manually by directing attention to the specific portion of data. However, selections of suitable features are important for the success of an abnormality detection system. Designing and selecting appropriate features are time-consuming, requires expensive domain knowledge and human labor. Further, it is very challenging to represent high-level concepts of abnormality in terms of raw input. Most of the existing abnormality detection system use handcrafted feature detector and are based on shallow architecture. In this work, we explore Deep Belief Network for abnormality detection and simultaneously, compared the performance of classic neural network in terms of features learned and accuracy of detecting the abnormality. Further, we explore the set of features learn by each layer of the deep architecture. We also provide a simple and fast mechanism to visualize the feature at the higher layer. Further, the effect of different activation function on abnormality detection is also compared. We observed that deep learning based approach can be used for detecting an abnormality. It has better performance compare to classical neural network in separating distinct as well as almost similar data.

Lee, Sang Hyun, Oh, Sang Won, Jo, Hye Seon, Na, Man Gyun.  2021.  Abnormality Diagnosis in NPP Using Artificial Intelligence Based on Image Data. 2021 5th International Conference on System Reliability and Safety (ICSRS). :103–107.
Accidents in Nuclear Power Plants (NPPs) can occur for a variety of causes. However, among these, the scale of accidents due to human error can be greater than expected. Accordingly, researches are being actively conducted using artificial intelligence to reduce human error. Most of the research shows high performance based on the numerical data on NPPs, but the expandability of researches using only numerical data is limited. Therefore, in this study, abnormal diagnosis was performed using artificial intelligence based on image data. The methods applied to abnormal diagnosis are the deep neural network, convolution neural network, and convolution recurrent neural network. Consequently, in nuclear power plants, it is expected that the application of more methodologies can be expanded not only in numerical data but also in image-based data.
Donghoon Kim, Henry E. Schaffer, Mladen Vouk.  2015.  About PaaS Security. 3rd International IBM Cloud Academy Conference (ICACON 2015).
Kim, Donghoon, Schaffer, Henry E., Vouk, Mladen A..  2015.  About PaaS Security. 3rd International IBM Cloud Academy Conference (ICACON 2015).

Platform as a Service (PaaS) provides middleware resources to cloud customers. As demand for PaaS services increases, so do concerns about the security of PaaS. This paper discusses principal PaaS security and integrity requirements, and vulnerabilities and the corresponding countermeasures. We consider three core cloud elements: multi-tenancy, isolation, and virtualization and how they relate to PaaS services and security trends and concerns such as user and resource isolation, side-channel vulnerabilities in multi-tenant environments, and protection of sensitive data

Bilanová, Z., Perháč, J..  2019.  About possibilities of applying logical analysis of natural language in computer science. 2019 IEEE 13th International Symposium on Applied Computational Intelligence and Informatics (SACI). :251–256.
This paper deals with the comparison of the most popular methods of a logical analysis of natural language Montague intensional logic and Transparent intensional logic. At first, these logical apparatuses are compared in terms of their founding theoretical principles. Later, the selected sentence is examined through the logical analysis. The aim of the paper is to identify a more expressive logical method, which will be a suitable basis for the future design of an algorithm for the automated translation of the natural language into a formal representation of its meaning through a semantic machine.
Anashkin, Yegor V., Zhukova, Marina N..  2021.  About the System of Profiling User Actions Based on the Behavior Model. 2021 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (ElConRus). :191—195.
The paper considers the issue of increasing the level of trust to the user of the information system by applying profiling actions. The authors have developed the model of user behavior, which allows to identify the user by his actions in the operating system. The model uses a user's characteristic metric instead of binary identification. The user's characteristic demonstrates the degree to which the current actions of the user corresponding to the user's behavior model. To calculate the user's characteristic, several formulas have been proposed. The authors propose to implement the developed behavior model into the access control model. For this purpose, the authors create the prototype of the user action profiling system for Windows family operating systems. This system should control access to protected resources by analyzing user behavior. The authors performed a series of tests with this system. This allowed to evaluate the accuracy of the system based on the proposed behavior model. Test results showed the type I errors. Therefore, the authors invented and described a polymodel approach to profiling actions. Potentially, the polymodel approach should solve the problem of the accuracy of the user action profiling system.
Sanandaji, B.M., Bitar, E., Poolla, K., Vincent, T.L..  2014.  An abrupt change detection heuristic with applications to cyber data attacks on power systems. American Control Conference (ACC), 2014. :5056-5061.

We present an analysis of a heuristic for abrupt change detection of systems with bounded state variations. The proposed analysis is based on the Singular Value Decomposition (SVD) of a history matrix built from system observations. We show that monitoring the largest singular value of the history matrix can be used as a heuristic for detecting abrupt changes in the system outputs. We provide sufficient detectability conditions for the proposed heuristic. As an application, we consider detecting malicious cyber data attacks on power systems and test our proposed heuristic on the IEEE 39-bus testbed.
 

Hu, Zhengbing, Vasiliu, Yevhen, Smirnov, Oleksii, Sydorenko, Viktoriia, Polishchuk, Yuliia.  2019.  Abstract Model of Eavesdropper and Overview on Attacks in Quantum Cryptography Systems. 2019 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS). 1:399–405.
In today's world, it's almost impossible to find a sphere of human life in which information technologies would not be used. On the one hand, it simplifies human life - virtually everyone carries a mini-computer in his pocket and it allows to perform many operations, that took a lot of time, in minutes. In addition, IT has simplified and promptly developed areas such as medicine, banking, document circulation, military, and many other infrastructures of the state. Nevertheless, even today, privacy remains a major problem in many information transactions. One of the most important directions for ensuring the information confidentiality in open communication networks has been and remains its protection by cryptographic methods. Although it is known that traditional cryptography methods give reasons to doubt in their reliability, quantum cryptography has proven itself as a more reliable information security technology. As far is it quite new direction there is no sufficiently complete classification of attacks on quantum cryptography methods, in view of this new extended classification of attacks on quantum protocols and quantum cryptosystems is proposed in this work. Classification takes into account the newest attacks (which use devices loopholes) on quantum key distribution equipment. These attacks have been named \textbackslashtextless; \textbackslashtextless; quantum hacking\textbackslashtextgreater\textbackslashtextgreater. Such classification may be useful for choosing commercially available quantum key distribution system. Also abstract model of eavesdropper in quantum systems was created and it allows to determine a set of various nature measures that need to be further implemented to provide reliable security with the help of specific quantum systems.
Basin, David, Lochbihler, Andreas, Maurer, Ueli, Sefidgar, S. Reza.  2021.  Abstract Modeling of System Communication in Constructive Cryptography using CryptHOL. 2021 IEEE 34th Computer Security Foundations Symposium (CSF). :1–16.
Proofs in simulation-based frameworks have the greatest rigor when they are machine checked. But the level of details in these proofs surpasses what the formal-methods community can handle with existing tools. Existing formal results consider streamlined versions of simulation-based frameworks to cope with this complexity. Hence, a central question is how to abstract details from composability results and enable their formal verification.In this paper, we focus on the modeling of system communication in composable security statements. Existing formal models consider fixed communication patterns to reduce the complexity of their proofs. However, as we will show, this can affect the reusability of security statements. We propose an abstract approach to modeling system communication in Constructive Cryptography that avoids this problem. Our approach is suitable for mechanized verification and we use CryptHOL, a framework for developing mechanized cryptography proofs, to implement it in the Isabelle/HOL theorem prover. As a case study, we formalize the construction of a secure channel using Diffie-Hellman key exchange and a one-time-pad.
Abi-Antoun, Marwan, Khalaj, Ebrahim, Vanciu, Radu, Moghimi, Ahmad.  2016.  Abstract Runtime Structure for Reasoning About Security: Poster. Proceedings of the Symposium and Bootcamp on the Science of Security. :1–3.

We propose an interactive approach where analysts reason about the security of a system using an abstraction of its runtime structure, as opposed to looking at the code. They interactively refine a hierarchical object graph, set security properties on abstract objects or edges, query the graph, and investigate the results by studying highlighted objects or edges or tracing to the code. Behind the scenes, an inference analysis and an extraction analysis maintain the soundness of the graph with respect to the code.