A formal logic-based language and an automated verification tool for computer forensic investigation

The complexity of designing concurrent and highly-evolving interactive systems has grown to a point where system verification has become a hurdle. Fortunately, formal verification methods have arrived at the right time. They detect errors, inconsistencies and incompleteness at early development stages of a system formally modeled using a formal specification language. -calculus (Milner, 1999) is one such formal language which provides strong mathematical base that can be used for verifying system specifications. But manually verifying the specifications of concurrent systems is a very tedious and error-prone work, especially if the specifications are large. Consequently, an automated verification tool would be essential for efficient system design and development. In addition, formal verification tools are vital ingredient to fully harness the potential of component-based software composition. The authors developed such an automated verification tool which is highly portable and seamlessly integrates with the visualization, reduction and performance evaluation tools introduced (Ahmad & Rahimi, 2008; Rahimi, 2006; Rahimi et al., 2001, 2008) to provide a comprehensive tool for designing and analyzing multi process/agent systems. Open-Bisimulation (Sangiorgi, 1996) concept is utilized as the theoretical base for the design and implementation of the tool which incorporates an expert system implemented in Java Expert System Shell (JESS) (Friedman-Hill, 2003).

Download Full-text

Formal Verification of Secrecy, Coercion Resistance and Verifiability Properties for a Remote Electronic Voting Protocol

International Journal of Information Security and Privacy ◽

10.4018/jisp.2013040104 ◽

2013 ◽

Vol 7 (2) ◽

pp. 57-85

Author(s):

Khaoula Marzouki ◽

Amira Radhouani ◽

Narjes Ben Rajeb

Keyword(s):

Formal Verification ◽

Electronic Voting ◽

Automated Verification ◽

Verification Tool ◽

Verification Methods ◽

Pi Calculus ◽

Security Properties

Electronic voting protocols have many advantages over traditional voting but they are complex and subject to many kinds of attacks. Therefore, the use of formal verification methods is crucial to ensure some security properties. We propose to model a recent protocol of remote electronic voting in the applied Pi-calculus. We focalized on some security properties such as fairness which expresses the impossibility of obtaining partial results, eligibility which requires that only legitimate voters can vote, coercion resistance which ensures that no voter may vote under pressure, and verifiability which supposes that anyone can verify the accuracy of the final result. We proved either manually or using the automated verification tool ProVerif that the protocol satisfies these security properties.

Download Full-text

Automated Verification Tool for DHTML

21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06) ◽

10.1109/ase.2006.21 ◽

2006 ◽

Cited By ~ 1

Author(s):

Takaaki Tateishi ◽

Hisashi Miyashita ◽

Kouichi Ono ◽

Shin Saito

Keyword(s):

Automated Verification ◽

Verification Tool

Download Full-text

Forensic analysis of video steganography tools

10.7287/peerj.preprints.1019v2 ◽

2015 ◽

Author(s):

Thomas Sloan ◽

Julio Hernandez-Castro

Keyword(s):

State Of The Art ◽

Freedom Of Speech ◽

Forensic Analysis ◽

Forensic Investigation ◽

Video Steganography ◽

The Past ◽

Current State ◽

Hidden Data ◽

Computer Forensic ◽

Privacy And Anonymity

Steganography is the art and science of concealing information in such a way that only the sender and intended recipient of a message should be aware of its presence. Digital steganography has been used in the past on a variety of media including executable files, audio, text, games and, notably, images. Additionally, there is increasing research interest towards the use of video as a media for steganography, due to its pervasive nature and diverse embedding capabilities. In this work, we examine the embedding algorithms and other security characteristics of several video steganography tools. We show how all feature basic and severe security weaknesses. This is potentially a very serious threat to the security, privacy and anonymity of their users. It is important to highlight that most steganography users have perfectly legal and ethical reasons to employ it. Some common scenarios would include citizens in oppressive regimes whose freedom of speech is compromised, people trying to avoid massive surveillance or censorship, political activists, whistle blowers, journalists, etc. As a result of our findings, we strongly recommend to cease any use of these tools, and to remove any contents that may have been hidden, and any carriers stored, exchanged and/or uploaded online. For many of these tools, carrier files will be trivial to detect, potentially compromising any hidden data and the parties involved in the communication. We finish this work by presenting our steganalytic results, that highlight a very poor current state of the art in practical video steganography tools. There is unfortunately a complete lack of secure and publicly available tools, and even commercial tools offer very poor security. We therefore encourage the steganography community to work towards the development of more secure and accessible video steganography tools, and make them available for the general public. The results presented in this work can also be seen as a useful resource for forensic examiners to determine the existence of any video steganography materials over the course of a computer forensic investigation.

Download Full-text

RESEARCH ON COMPUTER EQUIPMENT AND SOFTWARE PRODUCTS IN INVESTIGATION OF CRIMES RELATED TO ILLEGAL TRAFFICKING OF DRUGS, PSYCHOTROPIC SUBSTANCES OR THEIR ANALOGUES

Theory and Practice of Forensic Science and Criminalistics ◽

10.32353/khrife.2.2020.30 ◽

2021 ◽

Vol 22 (2) ◽

Author(s):

M. Zelena

Keyword(s):

Drug Trafficking ◽

Information Technologies ◽

The Internet ◽

Web Browsers ◽

Forensic Investigation ◽

Software Products ◽

Psychotropic Substances ◽

Modern Information ◽

Computer Forensic ◽

Narcotic Drugs

This article outlines current issues of research on computer traces in the investigation of crimes at the stage of pre-trial investigation related to illegal trafficking of narcotic drugs, psychotropic substances or their analogues. The main ways of conducting drug trafficking in Ukraine using modern information technologies, that is, using computer technology (mostly mobile devices, personal portable computers) and software products (programs for communicating by means of calls and messages through the Internet, Web browsers, etc.) on the World Wide Web are analyzed. Based on the analysis of research and publications of scientists as well as on the basis of empirical research during computer forensic investigations connected with investigation of illegal distribution of narcotic drugs, methods of illicit goods distribution on the Internet along with methods for investigating computer technologies, which directly relate to drug trafficking using modern information technologies, has been considered. Types of data that can be extracted using specialized software in laboratories of computer research during computer forensic investigation, and which, in turn, can function as factual data and is the evidence of commission of crimes related to drug trafficking, psychotropic substances or their analogues are considered, namely, we are talking about such data as: information from messenger programs, web browsers, text messages, as well as from user files (including graphic, audio and video files); In addition, guiding questions that can be addressed to a forensic expert while computer forensic investigation in criminal investigations related to illegal production, manufacture, purchase, storage, transportation, transfer, sale of narcotic drugs, psychotropic substances or their analogues are suggested.

Download Full-text