Proving Reliability of Image Processing Techniques in Digital Forensics Applications

Binary images have found its place in many applications, such as digital forensics involving legal documents, authentication of images, digital books, contracts, and text recognition. Modern digital forensics applications involve binary image processing as part of data hiding techniques for ownershi...

Full description

Saved in:
Bibliographic Details
Published in:Security and communication networks 2022, Vol.2022, p.1-17
Main Authors: Iqbal, Saima, Khan, Wilayat, Alothaim, Abdulrahman, Qamar, Aamir, Alhudhaif, Adi, Alsubai, Shtwai
Format: Article
Language:English
Subjects:
Algorithms
Color imagery
Computer forensics
Digital imaging
Forensic computing
Forensic sciences
Formal method
Hard disks
High level languages
Image processing
Object recognition
Reliability analysis
Safety
Software
Transformations
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Binary images have found its place in many applications, such as digital forensics involving legal documents, authentication of images, digital books, contracts, and text recognition. Modern digital forensics applications involve binary image processing as part of data hiding techniques for ownership protection, copyright control, and authentication of digital media. Whether in image forensics, health, or other fields, such transformations are often implemented in high-level languages without formal foundations. The lack of formal foundation questions the reliability of the image processing techniques and hence the forensic results loose their legal significance. Furthermore, counter-forensics can impede or mislead the forensic analysis of the digital images. To ensure that any image transformation meet high standards of safety and reliability, more rigorous methods should be applied to image processing applications. To verify the reliability of these transformations, we propose to use formal methods based on theorem proving that can fulfil high standards of safety. To formally investigate binary image processing, in this paper, a reversible formal model of the binary images is defined in the Proof Assistant Coq. Multiple image transformation methods are formalized and their reliability properties are proved. To analyse real-life RGB images, a prototype translator is developed that reads RGB images and translate them to Coq definitions. As the formal definitions and proof scripts can be validated automatically by the computer, this raises the reliability and legal significance of the image forensic applications.
ISSN:1939-0114
1939-0122
DOI:10.1155/2022/1322264