Search results for: claim verification

Authors: Johannes Buchmann, Markus Kaiser

Abstract:

We decribe a formal specification and verification of the Rabin public-key scheme in the formal proof system Is-abelle/HOL. The idea is to use the two views of cryptographic verification: the computational approach relying on the vocabulary of probability theory and complexity theory and the formal approach based on ideas and techniques from logic and programming languages. The analysis presented uses a given database to prove formal properties of our implemented functions with computer support. Thema in task in designing a practical formalization of correctness as well as security properties is to cope with the complexity of cryptographic proving. We reduce this complexity by exploring a light-weight formalization that enables both appropriate formal definitions as well as eficient formal proofs. This yields the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Consequently, we get reliable proofs with a minimal error rate augmenting the used database. This provides a formal basis for more computer proof constructions in this area.

Keywords: public-key encryption, Rabin public-key scheme, formalproof system, higher-order logic, formal verification.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1580

Authors: M. Celeska, K. Najdenkoski, V. Dimchev, V. Stoilkov

Abstract:

Accurate determination of wind turbine performance is necessary for economic operation of a wind farm. At present, the procedure to carry out the power performance verification of wind turbines is based on a standard of the International Electrotechnical Commission (IEC). In this paper, nonparametric statistical inference is applied to designing a simple, inexpensive method of verifying the power performance of a wind turbine. A statistical test is explained, examined, and the adequacy is tested over real data. The methods use the information that is collected by the SCADA system (Supervisory Control and Data Acquisition) from the sensors embedded in the wind turbines in order to carry out the power performance verification of a wind farm. The study has used data on the monthly output of wind farm in the Republic of Macedonia, and the time measuring interval was from January 1, 2016, to December 31, 2016. At the end, it is concluded whether the power performance of a wind turbine differed significantly from what would be expected. The results of the implementation of the proposed methods showed that the power performance of the specific wind farm under assessment was acceptable.

Keywords: Canonical correlation analysis, power curve, power performance, wind energy.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1006

Authors: Kriddikorn Kaewwongsri, Nikom Suvonvorn

Abstract:

In the deep south of Thailand, checkpoints for people verification are necessary for the security management of risk zones, such as official buildings in the conflict area. In this paper, we propose an automatic checkpoint system that verifies persons using information from ID cards and facial features. The methods for a person’s information abstraction and verification are introduced based on useful information such as ID number and name, extracted from official cards, and facial images from videos. The proposed system shows promising results and has a real impact on the local society.

Keywords: Face comparison, card recognition, OCR, checkpoint system, authentication.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1777

Authors: Li-Li Li, Jinghai Feng, Lixin Song

Abstract:

This paper evaluates the dividend payments for general claim size distributions in the presence of a dividend barrier. The surplus of a company is modeled using the classical risk process perturbed by diffusion, and in addition, it is assumed to accrue interest at a constant rate. After presenting the integro-differential equation with initial conditions that dividend payments satisfies, the paper derives a useful expression of the dividend payments by employing the theory of Volterra equation. Furthermore, the optimal value of dividend barrier is found. Finally, numerical examples illustrate the optimality of optimal dividend barrier and the effects of parameters on dividend payments.

Keywords: Dividend payout, Integro-differential equation, Jumpdiffusion model, Volterra equation

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1783

Authors: Patrick O. Bobbie, Prince S. Attrams

Abstract:

In recent times, the rapid change in new technologies has spurred up the way and manner records are handled in educational institutions. Also, there is a need for reliable access and ease-of use to these records, resulting in increased productivity in organizations. In academic institutions, such benefits help in quality assessments, institutional performance, and assessments of teaching and evaluation methods. Students in educational institutions benefit the most when advanced technologies are deployed in accessing records. This research paper discusses the use of biometric technologies coupled with smartcard technologies to provide a unique way of identifying students and matching their data to financial records to grant them access to restricted areas such as examination halls. The system developed in this paper, has an identity verification component as part of its main functionalities. A systematic software development cycle of analysis, design, coding, testing and support was used. The system provides a secured way of verifying student’s identity and real time verification of financial records. An advanced prototype version of the system has been developed for testing purposes.

Keywords: Biometrics, fingerprints, identity-verification, smartcards.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2038

Authors: Ahmed Kamil Hasan Al-Ali, Bouchra Senadji, Ganesh Naik

Abstract:

We propose a system to real environmental noise and channel mismatch for forensic speaker verification systems. This method is based on suppressing various types of real environmental noise by using independent component analysis (ICA) algorithm. The enhanced speech signal is applied to mel frequency cepstral coefficients (MFCC) or MFCC feature warping to extract the essential characteristics of the speech signal. Channel effects are reduced using an intermediate vector (i-vector) and probabilistic linear discriminant analysis (PLDA) approach for classification. The proposed algorithm is evaluated by using an Australian forensic voice comparison database, combined with car, street and home noises from QUT-NOISE at a signal to noise ratio (SNR) ranging from -10 dB to 10 dB. Experimental results indicate that the MFCC feature warping-ICA achieves a reduction in equal error rate about (48.22%, 44.66%, and 50.07%) over using MFCC feature warping when the test speech signals are corrupted with random sessions of street, car, and home noises at -10 dB SNR.

Keywords: Noisy forensic speaker verification, ICA algorithm, MFCC, MFCC feature warping.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 972

Authors: N. Boudiaf

Abstract:

One major difficulty that faces developers of concurrent and distributed software is analysis for concurrency based faults like deadlocks. Petri nets are used extensively in the verification of correctness of concurrent programs. ECATNets are a category of algebraic Petri nets based on a sound combination of algebraic abstract types and high-level Petri nets. ECATNets have 'sound' and 'complete' semantics because of their integration in rewriting logic and its programming language Maude. Rewriting logic is considered as one of very powerful logics in terms of description, verification and programming of concurrent systems We proposed previously a method for translating Ada-95 tasking programs to ECATNets formalism (Ada-ECATNet) and we showed that ECATNets formalism provides a more compact translation for Ada programs compared to the other approaches based on simple Petri nets or Colored Petri nets. We showed also previously how the ECATNet formalism offers to Ada many validation and verification tools like simulation, Model Checking, accessibility analysis and static analysis. In this paper, we describe the implementation of our translation of the Ada programs into ECATNets.

Keywords: Ada tasking, Analysis, Automatic Translation, ECATNets, Maude, Rewriting Logic.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1576

Authors: Sebastian Kusch, Markus Kaiser

Abstract:

In this paper we analyze the application of a formal proof system to the discrete logarithm problem used in publickey cryptography. That means, we explore a computer verification of the ElGamal encryption scheme with the formal proof system Isabelle/HOL. More precisely, the functional correctness of this algorithm is formally verified with computer support. Besides, we present a formalization of the DSA signature scheme in the Isabelle/HOL system. We show that this scheme is correct what is a necessary condition for the usefulness of any cryptographic signature scheme.

Keywords: Formal proof system, higher-order logic, formal verification, cryptographic signature scheme.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1546

Authors: Zeeshan Furqan, Shahabuddin Muhammad, Ratan Guha

Abstract:

IEEE has designed 802.11i protocol to address the security issues in wireless local area networks. Formal analysis is important to ensure that the protocols work properly without having to resort to tedious testing and debugging which can only show the presence of errors, never their absence. In this paper, we present the formal verification of an abstract protocol model of 802.11i. We translate the 802.11i protocol into the Strand Space Model and then prove the authentication property of the resulting model using the Strand Space formalism. The intruder in our model is imbued with powerful capabilities and repercussions to possible attacks are evaluated. Our analysis proves that the authentication of 802.11i is not compromised in the presented model. We further demonstrate how changes in our model will yield a successful man-in-the-middle attack.

Keywords: authentication, formal analysis, formal verification, security.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1504

Authors: Shuzhen Yao, Fengjing Zhao, Jianwei He

Abstract:

The UML modeling of complex distributed systems often is a great challenge due to the large amount of parallel real-time operating components. In this paper the problems of verification of such systems are discussed. ECPN, an Extended Colored Petri Net is defined to formally describe state transitions of components and interactions among components. The relationship between sequence diagrams and Free Choice Petri Nets is investigated. Free Choice Petri Net theory helps verifying the liveness of sequence diagrams. By converting sequence diagrams to ECPNs and then comparing behaviors of sequence diagram ECPNs and statecharts, the consistency among models is analyzed. Finally, a verification process for an example model is demonstrated.

Keywords: Consistency, liveness, Petri Net, sequence diagram.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1594

Authors: J. Novak-Marcincin, J. Barna, M. Janak

Abstract:

Augmented Reality (AR) shows great promises for its usage as a tool for simulation and verification of design proposal of new technological systems. Main advantage of augmented reality application usage is possibility of creation and simulation of new technological unit before its realization. This may contribute to increasing of safety and ergonomics and decreasing of economical aspects of new proposed unit. Virtual model of proposed workcell could reveal hidden errors which elimination in later stage of new workcell creation should cause great difficulties. Paper describes process of such virtual model creation and possibilities of its simulation and verification by augmented reality tools.

Keywords: Augmented reality, simulation, workcell design.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1678

Authors: Siamak Rasulzadeh

Abstract:

Graph transformation has recently become more and more popular as a general visual modeling language to formally state the dynamic semantics of the designed models. Especially, it is a very natural formalism for languages which basically are graph (e.g. UML). Using this technique, we present a highly understandable yet precise approach to formally model and analyze the behavioral semantics of UML 2.0 Activity diagrams. In our proposal, AGG is used to design Activities, then using our previous approach to model checking graph transformation systems, designers can verify and analyze designed Activity diagrams by checking the interesting properties as combination of graph rules and LTL (Linear Temporal Logic) formulas on the Activities.

Keywords: UML 2.0 Activity, Verification, Model Checking, Graph Transformation, Dynamic Semantics.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1435

Authors: Tamara Nestorović, Jean Lefèvre, Stefan Ringwelski, Ulrich Gabbert

Abstract:

Two approaches for model development of a smart acoustic box are suggested in this paper: the finite element (FE) approach and the subspace identification. Both approaches result in a state-space model, which can be used for obtaining the frequency responses and for the controller design. In order to validate the developed FE model and to perform the subspace identification, an experimental set-up with the acoustic box and dSPACE system was used. Experimentally obtained frequency responses show good agreement with the frequency responses obtained from the FE model and from the identified model.

Keywords: Acoustic box, experimental verification, finite element model, subspace identification.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1551

Authors: Daxing Wang, Jikai Teng

Abstract:

An aggregate signature scheme can aggregate n signatures on n distinct messages from n distinct signers into a single signature. Thus, n verification equations can be reduced to one. So the aggregate signature adapts to Mobile Ad hoc Network (MANET). In this paper, we propose an efficient ID-based aggregate signature scheme with constant pairing computations. Compared with the existing ID-based aggregate signature scheme, this scheme greatly improves the efficiency of signature communication and verification. In addition, in this work, we apply our ID-based aggregate sig- nature to authenticated routing protocol to present a secure routing scheme. Our scheme not only provides sound authentication and a secure routing protocol in ad hoc networks, but also meets the nature of MANET.

Keywords: Identity-based cryptography, Aggregate signature, Bilinear pairings, Authenticated routing scheme.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2094

Authors: Quoc-Nam Tran

Abstract:

The theory of Groebner Bases, which has recently been honored with the ACM Paris Kanellakis Theory and Practice Award, has become a crucial building block to computer algebra, and is widely used in science, engineering, and computer science. It is wellknown that Groebner bases computation is EXP-SPACE in a general setting. In this paper, we give an algorithm to show that Groebner bases computation is P-SPACE in Boolean rings. We also show that with this discovery, the Groebner bases method can theoretically be as efficient as other methods for automated verification of hardware and software. Additionally, many useful and interesting properties of Groebner bases including the ability to efficiently convert the bases for different orders of variables making Groebner bases a promising method in automated verification.

Keywords: Algorithm, Complexity, Groebner basis, Applications of Computer Science.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1818

Authors: Shin-Jer Yang, Kai-Tai Yang

Abstract:

In response to a changing world and the fast growth of the Internet, more and more enterprises are replacing web-based services with cloud-based ones. Multi-tenancy technology is becoming more important especially with Software as a Service (SaaS). This in turn leads to a greater focus on the application of Identity and Access Management (IAM). Conventional Near-Field Communication (NFC) based verification relies on a computer browser and a card reader to access an NFC tag. This type of verification does not support mobile device login and user-based access management functions. This study designs an NFC-based third-party cloud identity and access management scheme (NFC-IAM) addressing this shortcoming. Data from simulation tests analyzed with Key Performance Indicators (KPIs) suggest that the NFC-IAM not only takes less time in identity identification but also cuts time by 80% in terms of two-factor authentication and improves verification accuracy to 99.9% or better. In functional performance analyses, NFC-IAM performed better in salability and portability. The NFC-IAM App (Application Software) and back-end system to be developed and deployed in mobile device are to support IAM features and also offers users a more user-friendly experience and stronger security protection. In the future, our NFC-IAM can be employed to different environments including identification for mobile payment systems, permission management for remote equipment monitoring, among other applications.

Keywords: Cloud service, multi-tenancy, NFC, IAM, mobile device.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1108

Authors: Ivana Mokrá

Abstract:

The article deals with modelling of the fire pragmatism in the area of military management and its experimental verification. Potential approaches are based on the synergy of mathematical and theoretical ideas, operational and tactical requirements and the military decision-making process. This issue has taken on importance in recent times, particularly with the increasing trend of digitized battlefield, the development of C4ISR systems and intention to streamline the command and control process at the lowest levels of command. From fundamental and philosophical point of view, these new approaches seek to significantly upgrade and enhance the decision-making process of the tactical commanders.

Keywords: Military management, decision-making process, strike modeling, experimental evaluation, pragmatism, tactical strike modeling

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1519

Authors: Miklos Taliga

Abstract:

In the present case study we examined the development and testing methods of systems that contain safety-critical elements in different industrial fields. Consequentially, we observed the classical object-oriented development and testing environment, as both medical technology and automobile industry approaches the development of safety critical elements that way. Subsequently, we examined model-based development. We introduce the quality parameters that define development and testing. While taking modern agile methodology (scrum) into consideration, we examined whether and to what extent the methodologies we found fit into this environment.

Keywords: Safety-critical elements, quality management, unit verification, model base testing, agile methods, scrum, metamodel, object-oriented programming, field specific modelling, sprint, user story, UML Standard.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 811

Authors: A. Jalal, S. Kim

Abstract:

Different methods containing biometric algorithms are presented for the representation of eigenfaces detection including face recognition, are identification and verification. Our theme of this research is to manage the critical processing stages (accuracy, speed, security and monitoring) of face activities with the flexibility of searching and edit the secure authorized database. In this paper we implement different techniques such as eigenfaces vector reduction by using texture and shape vector phenomenon for complexity removal, while density matching score with Face Boundary Fixation (FBF) extracted the most likelihood characteristics in this media processing contents. We examine the development and performance efficiency of the database by applying our creative algorithms in both recognition and detection phenomenon. Our results show the performance accuracy and security gain with better achievement than a number of previous approaches in all the above processes in an encouraging mode.

Keywords: Ubiquitous architecture, verification, Identification, recognition

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1309

Authors: Rasheed Gbenga Jimoh, Akinbowale Nathaniel Babatunde

Abstract:

The use of Automated Teller Machine (ATM) has become an important tool among commercial banks, customers of banks have come to depend on and trust the ATM conveniently meet their banking needs. Although the overwhelming advantages of ATM cannot be over-emphasized, its alarming fraud rate has become a bottleneck in it’s full adoption in Nigeria. This study examined the menace of ATM in the society another cost of running ATM services by banks in the country. The researcher developed a prototype of an enhanced Automated Teller Machine Authentication using Short Message Service (SMS) Verification. The developed prototype was tested by Ten (10) respondents who are users of ATM cards in the country and the data collected was analyzed using Statistical Package for Social Science (SPSS). Based on the results of the analysis, it is being envisaged that the developed prototype will go a long way in reducing the alarming rate of ATM fraud in Nigeria.

Keywords: ATM, ATM Fraud, E-banking, Prototyping.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2166

Authors: Y. V. Kim

Abstract:

This article presents an approach with regards to the Functional Testing of Space System (SS) that could be a space vehicle (spacecraft-S/C) and/or its equipment and components – S/C subsystems. This test should finalize the Space Qualification Tests (SQT) campaign. It could be considered as a generic test and used for a wide class of SS that, from the point of view of System Dynamics and Control Theory, may be described by the ordinary differential equations. The suggested methodology is based on using semi-natural experiment laboratory stand that does not require complicated, precise and expensive technological control-verification equipment. However, it allows for testing totally assembled system during Assembling, Integration and Testing (AIT) activities at the final phase of SQT, involving system hardware (HW) and software (SW). The test physically activates system input (sensors) and output (actuators) and requires recording their outputs in real time. The data are then inserted in a laboratory computer, where it is post-experiment processed by the MATLAB/Simulink Identification Toolbox. It allows for estimating the system dynamics in the form of estimation of its differential equation coefficients through the verification experimental test and comparing them with expected mathematical model, prematurely verified by mathematical simulation during the design process. Mathematical simulation results presented in the article show that this approach could be applicable and helpful in SQT practice. Further semi-natural experiments should specify detail requirements for the test laboratory equipment and test-procedures.

Keywords: system dynamics, space system ground tests, space qualification, system dynamics identification, satellite attitude control, assembling integration and testing

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 520

Authors: George Eleftherakis, Petros Kefalas, Anna Sotiriadou, Evangelos Kehris

Abstract:

Recent advances in both the testing and verification of software based on formal specifications of the system to be built have reached a point where the ideas can be applied in a powerful way in the design of agent-based systems. The software engineering research has highlighted a number of important issues: the importance of the type of modeling technique used; the careful design of the model to enable powerful testing techniques to be used; the automated verification of the behavioural properties of the system; the need to provide a mechanism for translating the formal models into executable software in a simple and transparent way. This paper introduces the use of the X-machine formalism as a tool for modeling biology inspired agents proposing the use of the techniques built around X-machine models for the construction of effective, and reliable agent-based software systems.

Keywords: Biology inspired agent, formal methods, x-machines.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1487

Authors: Omaima Bamasak

Abstract:

This paper presents a novel method that allows an agent host to delegate its signing power to an anonymous mobile agent in such away that the mobile agent does not reveal any information about its host-s identity and, at the same time, can be authenticated by the service host, hence, ensuring fairness of service provision. The solution introduces a verification server to verify the signature generated by the mobile agent in such a way that even if colluding with the service host, both parties will not get more information than what they already have. The solution incorporates three methods: Agent Signature Key Generation method, Agent Signature Generation method, Agent Signature Verification method. The most notable feature of the solution is that, in addition to allowing secure and anonymous signature delegation, it enables tracking of malicious mobile agents when a service host is attacked. The security properties of the proposed solution are analyzed, and the solution is compared with the most related work.

Keywords: Anonymous signature delegation, collusion resistance, e-commerce fairness, mobile agent security.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1431

Authors: C. Guven, M. Tufekci, E. Bayik, O. Gedik, M. Tas

Abstract:

A sliding door system is used in commercial vehicles and passenger cars to allow a larger unobstructed access to the interior for loading and unloading. The movement of a sliding door on vehicle body is ensured by mechanisms and tracks having special cross-section which is manufactured by roll forming and stretch bending process. There are three tracks and three mechanisms which are called upper, central and lower on a sliding door system. There are static requirements as strength on different directions, rigidity for mechanisms, door drop off, door sag; dynamic requirements as high energy slam opening-closing and durability requirement to validate these products. In addition, there is a kinematic requirement to find out force values from door handle during manual operating. In this study, finite element analysis and physical test results which are realized for sliding door systems will be shared comparatively.

Keywords: Finite element analysis, sliding door, experimental, verification, vehicle tests.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 3078

Authors: A. L. Qureshi, A. A. Mahessar, A. Baloch

Abstract:

Flood wave propagation in river channel flow can be enunciated by nonlinear equations of motion for unsteady flow. It is difficult to find analytical solution of these non-linear equations. Hence, in this paper verification of the finite element model has been carried out against available numerical predictions and field data. The results of the model indicate a good matching with both Preissmann scheme and HEC-RAS model for a river reach of 29km at both sites (15km from upstream and at downstream end) for discharge hydrographs. It also has an agreeable comparison with the Preissemann scheme for the flow depth (stage) hydrographs. The proposed model has also been applying to forecast daily discharges at 400km downstream in the Indus River from Sukkur barrage of Sindh, Pakistan, which demonstrates accurate model predictions with observed the daily discharges. Hence, this model may be utilized for flood warnings in advance.

Keywords: Finite Element Method, Flood Forecasting, HEC-RAS, Indus river.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 2670

Authors: M. Matash Borujerdi, S.M. Mirzababaei

Abstract:

As computer network technology becomes increasingly complex, it becomes necessary to place greater requirements on the validity of developing standards and the resulting technology. Communication networks are based on large amounts of protocols. The validity of these protocols have to be proved either individually or in an integral fashion. One strategy for achieving this is to apply the growing field of formal methods. Formal methods research defines systems in high order logic so that automated reasoning can be applied for verification. In this research we represent and implement a formerly announced multicast protocol in Prolog language so that certain properties of the protocol can be verified. It is shown that by using this approach some minor faults in the protocol were found and repaired. Describing the protocol as facts and rules also have other benefits i.e. leads to a process-able knowledge. This knowledge can be transferred as ontology between systems in KQML format. Since the Prolog language can increase its knowledge base every time, this method can also be used to learn an intelligent network.

Keywords: Formal methods, MobiCast, Mobile Network, Multicast.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1364

Authors: M. Sarrab, H. Bourdoucen

Abstract:

Mobile applications are verified to check the correctness or evaluated to check the performance with respect to specific security properties such as Availability, Integrity and Confidentiality. Where they are made available to the end users of the mobile application is achievable only to a limited degree using software engineering static verification techniques. The more sensitive the information, such as credit card data, personal medical information or personal emails being processed by mobile application, the more important it is to ensure the confidentiality of this information. Monitoring untrusted mobile application during execution in an environment where sensitive information is present is difficult and unnerving. The paper addresses the issue of monitoring and controlling the flow of confidential information during untrusted mobile application execution. The approach concentrates on providing a dynamic and usable information security solution by interacting with the mobile users during the runtime of mobile application in response to information flow events.

Keywords: Mobile application, Run-time verification, Usable security, Direct information flow.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1944

Authors: Manasjyoti Bhuyan, Kandarpa Kumar Sarma, Hirendra Das

Abstract:

Signature represents an individual characteristic of a person which can be used for his / her validation. For such application proper modeling is essential. Here we propose an offline signature recognition and verification scheme which is based on extraction of several features including one hybrid set from the input signature and compare them with the already trained forms. Feature points are classified using statistical parameters like mean and variance. The scanned signature is normalized in slant using a very simple algorithm with an intention to make the system robust which is found to be very helpful. The slant correction is further aided by the use of an Artificial Neural Network (ANN). The suggested scheme discriminates between originals and forged signatures from simple and random forgeries. The primary objective is to reduce the two crucial parameters-False Acceptance Rate (FAR) and False Rejection Rate (FRR) with lesser training time with an intension to make the system dynamic using a cluster of ANNs forming a multiple classifier system.

Keywords: offline, algorithm, FAR, FRR, ANN.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1764

Authors: Alexander V. Libin, Manon Schladen, Assya Pascalev, Nawar Shara, Miriam Philmon, Yuri Millo, Joseph Verbalis

Abstract:

Chronic conditions carry with them strong emotions and often lead to charged relationships between patients and their health providers and, by extension, patients and health researchers. Persons are both autonomous and relational and a purely cognitive model of autonomy neglects the social and relational basis of chronic illness. Ensuring genuine informed consent in research requires a thorough understanding of how participants perceive a study and their reasons for participation. Surveys may not capture the complexities of reasoning that underlies study participation. Contradictory reasons for participation, for instance an initial claim of altruism as rationale and a subsequent claim of personal benefit (therapeutic misconception), affect the quality of informed consent. Individuals apply principles through the filter of personal values and lived experience. Authentic autonomy, and hence authentic consent to research, occurs within the context of patients- unique life narratives and illness experiences.

Keywords: ethical dilemmas, open source technology, patient education, psychology of decision making

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 1796

Authors: Mahesh Chudasama, Harit Raval

Abstract:

Conical sections and shells made from metal plates are widely used in various industrial applications. 3-roller conical bending process is preferably used to produce such conical sections and shells. Bending mechanics involved in the process is complex and little work is done in this area. In the present paper an analytical model is developed to predict bending force which will be acting during 3-roller conical bending process. To verify the developed model, conical bending experiments are performed. Analytical results and experimental results were compared. Force predicted by analytical model is in close proximity of the experimental results. The error in the prediction is ±10%. Hence the model gives quite satisfactory results. Present model is also compared with the previously published bending force prediction model and it is found that the present model gives better results. The developed model can be used to estimate the bending force during 3-roller bending process and can be useful to the designers for designing the 3-roller conical bending machine.

Keywords: Bending-force, Experimental-verification, Internal-moment, Roll-bending.

Procedia APA BibTeX Chicago EndNote Harvard JSON MLA RIS XML ISO 690 PDF Downloads 4008