Search results for: identity verification

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article we explore the application of a formal proof system to verification problems in cryptography. Cryptographic properties concerning correctness or security of some cryptographic algorithms are of great interest. Beside some basic lemmata, we explore an implementation of a complex function that is used in cryptography. More precisely, we describe formal properties of this implementation that we computer prove. We describe formalized probability distributions (σ-algebras, probability spaces and conditional probabilities). These are given in the formal language of the formal proof system Isabelle/HOL. Moreover, we computer prove Bayes- Formula. Besides, we describe an application of the presented formalized probability distributions to cryptography. Furthermore, this article shows that computer proofs of complex cryptographic functions are possible by presenting an implementation of the Miller- Rabin primality test that admits formal verification. Our achievements are a step towards computer verification of cryptographic primitives. They describe a basis for computer verification in cryptography. Computer verification can be applied to further problems in cryptographic research, if the corresponding basic mathematical knowledge is available in a database.

Keywords: prime numbers, primality tests, (conditional) probabilitydistributions, formal proof system, higher-order logic, formalverification, Bayes' Formula, Miller-Rabin primality test.

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

Authors: H. Buluthan Cetintas

Abstract:

Corporate identity, which has several advantages such that the employees become integrated with their corporations, corporation is distinguished from its competitors and it is recognized by the masses, is the total of the distinctive corporate features that and corporation has. That the information takes part in production as a more important component than labor and capital has required that the corporations are reorganized as information-based. Therefore, information and its management have reached a basic and prevalent position in having sustainable competitive advantage. Thanks to the information management which regulates the information and makes it reachable and available, information will be produced in line with a specific purpose in the corporations and be used in all the corporate processes. As an auxiliary power for increase in the economic potential, efficiency and productivity of the corporation, corporate identity consists of four components. These are corporate philosophy, corporate design, corporate behavior and corporate communication. In this study, the effects of the information management on corporate identity are discussed from the point of these four elements.

Keywords: Corporate identity, information management.

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

Authors: Kenan Cetinkaya, Semanur Kodan

Abstract:

Ahiska Turks in the Philadelphia area maintain a very complex, cultural heritage which they have carried with them for centuries from Georgia to Uzbekistan then Russia and lastly to the USA. While facing very severe conditions in the last half of the last century, their passion for their language, religion and tradition allowed them to keep their cultural identity. In the paper, the Ahiska Turks’ sorrowful story is reviewed and their struggle with keeping their identity in a multicultural environment of the USA is examined in the context of the Philadelphia area.

Keywords: Ahiska Turks, identity, integration, Philadelphia, Turkish

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

Authors: Adriano Bessa Albuquerque, Francisco Jose Barreto Nunes

Abstract:

Software vulnerabilities are increasing and not only impact services and processes availability as well as information confidentiality, integrity and privacy, but also cause changes that interfere in the development process. Security test could be a solution to reduce vulnerabilities. However, the variety of test techniques with the lack of real case studies of applying tests focusing on software development life cycle compromise its effective use. This paper offers an overview of how a Systematic Mapping Study (MS) about security verification, validation and test (VVT) was performed, besides presenting general results about this study.

Keywords: Software test, software security verification validation and test, security test institutionalization, systematic mapping study.

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

Authors: Vasiliki Vlachou, Christos Kontzinos, Ourania Markaki, Panagiotis Kokkinakos, Vagelis Karakolis, John Psarras

Abstract:

Higher Education is resisting the pull of technology, especially as this concerns the issuance and verification of degrees and certificates. It is widely known that education certificates are largely produced in paper form making them vulnerable to damage while holders of such certificates are dependent on the universities and other issuing organisations. QualiChain is an EU Horizon 2020 (H2020) research project aiming to transform and revolutionise the domain of public education and its ties with the job market by leveraging blockchain, analytics and decision support to develop a platform for the verification and sharing of education certificates. Blockchain plays an integral part in the QualiChain solution in providing a trustworthy environment to store, share and manage such accreditations. Under the context of this paper, three prominent blockchain platforms (Ethereum, Hyperledger Fabric, Hyperledger Iroha) were considered as a means of experimentation for creating a system with the basic functionalities that will be needed for trustworthy degree verification. The methodology and respective system developed and presented in this paper used Hyperledger Iroha and proved that this specific platform can be used to easily develop decentralize applications. Future papers will attempt to further experiment with other blockchain platforms and assess which has the best potential.

Keywords: Blockchain, degree verification, higher education certificates, Hyperledger Iroha.

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

Authors: Katsumi Wasaki, Naoki Iwasaki

Abstract:

Model-checking tools such as Symbolic Model Verifier (SMV) and NuSMV are available for checking hardware designs. These tools can automatically check the formal legitimacy of a design. However, NuSMV is too low level for describing a complete hardware design. It is therefore necessary to translate the system definition, as designed in a language such as Verilog or VHDL, into a language such as NuSMV for validation. In this paper, we present a meta hardware description language, Melasy, that contains a code generator for existing hardware description languages (HDLs) and languages for model checking that solve this problem.

Keywords: meta description language, software/hardware codesign, co-verification, formal verification, hardware compiler, modelchecking.

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

Authors: T. Jayanthi, K. Velusamy, H. Seetha, S. A. V. Satya Murty

Abstract:

Verification and Validation of Simulated Process Model is the most important phase of the simulator life cycle. Evaluation of simulated process models based on Verification and Validation techniques checks the closeness of each component model (in a simulated network) with the real system/process with respect to dynamic behaviour under steady state and transient conditions. The process of Verification and Validation helps in qualifying the process simulator for the intended purpose whether it is for providing comprehensive training or design verification. In general, model verification is carried out by comparison of simulated component characteristics with the original requirement to ensure that each step in the model development process completely incorporates all the design requirements. Validation testing is performed by comparing the simulated process parameters to the actual plant process parameters either in standalone mode or integrated mode. A Full Scope Replica Operator Training Simulator for PFBR - Prototype Fast Breeder Reactor has been developed at IGCAR, Kalpakkam, INDIA named KALBR-SIM (Kalpakkam Breeder Reactor Simulator) where in the main participants are engineers/experts belonging to Modeling Team, Process Design and Instrumentation & Control design team. This paper discusses about the Verification and Validation process in general, the evaluation procedure adopted for PFBR operator training Simulator, the methodology followed for verifying the models, the reference documents and standards used etc. It details out the importance of internal validation by design experts, subsequent validation by external agency consisting of experts from various fields, model improvement by tuning based on expert’s comments, final qualification of the simulator for the intended purpose and the difficulties faced while co-coordinating various activities.

Keywords: Verification and Validation (V&V), Prototype Fast Breeder Reactor (PFBR), Kalpakkam Breeder Reactor Simulator (KALBR-SIM), Steady State, Transient State.

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

Authors: Kreetha Thumcharoensathit

Abstract:

The purpose of the analysis of Thai Arts and Culture which concerning the formation of Thai identity letter font designed is to identify The Aumphawa local community identity so as to select the suitable letter font which can applicable to the computer software usage. The populated survey was from the group of local people who live in Aumphawa sub-district. The methodological is cluster sampling from 100 surveyed, those 50 were from people who have household registration done in Aumphawa sub-district and other from people who live outside. In order to analyze and design the Thai identity letter font computer software designed for both Thai and English language version, the analysis had been completed by compiling of document and field survey from local people’s opinion on their Arts and Culture identity. The out-put will be submitted to the experts for evaluation.

Keywords: Thai Arts, Design, Font, Identity.

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

Authors: M. L. Anitha, K. A. Radhakrishna Rao

Abstract:

With the advent of modern computing technology, there is an increased demand for developing recognition systems that have the capability of verifying the identity of individuals. Recognition systems are required by several civilian and commercial applications for providing access to secured resources. Traditional recognition systems which are based on physical identities are not sufficiently reliable to satisfy the security requirements due to the use of several advances of forgery and identity impersonation methods. Recognizing individuals based on his/her unique physiological characteristics known as biometric traits is a reliable technique, since these traits are not transferable and they cannot be stolen or lost. Since the performance of biometric based recognition system depends on the particular trait that is utilized, the present work proposes a fusion approach which combines Inner knuckle print (IKP) trait of the middle, ring and index fingers with the geometrical features of hand. The hand image captured from a digital camera is preprocessed to find finger IKP as region of interest (ROI) and hand geometry features. Geometrical features are represented as the distances between different key points and IKP features are extracted by applying local binary pattern descriptor on the IKP ROI. The decision level AND fusion was adopted, which has shown improvement in performance of the combined scheme. The proposed approach is tested on the database collected at our institute. Proposed approach is of significance since both hand geometry and IKP features can be extracted from the palm region of the hand. The fusion of these features yields a false acceptance rate of 0.75%, false rejection rate of 0.86% for verification tests conducted, which is less when compared to the results obtained using individual traits. The results obtained confirm the usefulness of proposed approach and suitability of the selected features for developing biometric based recognition system based on features from palmar region of hand.

Keywords: Biometrics, hand geometry features, inner knuckle print, recognition.

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

Authors: Wang, Kuei-Ing, Jou-Fan Shih

Abstract:

This study adopts deterrence theory as well as social identities as moderators, and explores their moderating affects on online toxic disinhibition. Survey and Experimental methodologies are applied to test the research model and four hypotheses are developed in this study. The controllability of identity positively influenced the behavior of toxic disinhibition both in experimental and control groups while the fluidity of the identity did not have significant influences on online disinhibition. Punishment certainty, punishment severity as well as social identity negatively moderated the relation between the controllability of the identity and the toxic disinhibition. The result of this study shows that internet users hide their real identities when they behave inappropriately on internet, but once they acknowledge that the inappropriate behavior will be found and punished severely, the inappropriate behavior then will be weakened.

Keywords: Seductive properties of Internet, Online Disinhibition, Punishment Certainty, Punishment Severity, Social Identity.

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

Authors: Todsaporn Fuangrod, Daryl J. O'Connor, Boyd MC McCurdy, Peter B. Greer

Abstract:

An electronic portal image device (EPID) has become a method of patient-specific IMRT dose verification for radiotherapy. Research studies have focused on pre and post-treatment verification, however, there are currently no interventional procedures using EPID dosimetry that measure the dose in real time as a mechanism to ensure that overdoses do not occur and underdoses are detected as soon as is practically possible. As a result, an EPID-based real time dose verification system for dynamic IMRT was developed and was implemented with MATLAB/Simulink. The EPID image acquisition was set to continuous acquisition mode at 1.4 images per second. The system defined the time constraint gap, or execution gap at the image acquisition time, so that every calculation must be completed before the next image capture is completed. In addition, the <=-evaluation method was used for dose comparison, with two types of comparison processes; individual image and cumulative dose comparison monitored. The outputs of the system are the <=-map, the percent of <=<1, and mean-<= versus time, all in real time. Two strategies were used to test the system, including an error detection test and a clinical data test. The system can monitor the actual dose delivery compared with the treatment plan data or previous treatment dose delivery that means a radiation therapist is able to switch off the machine when the error is detected.

Keywords: real-time dose verification, EPID dosimetry, simulation, dynamic IMRT

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

Authors: Kaylash Chaudhary, Ansgar Fehnker

Abstract:

There are many virtual payment systems available to conduct micropayments. It is essential that the protocols satisfy the highest standards of correctness. This paper examines the Netpay Protocol [3], provide its formalization as automata model, and prove two important correctness properties, namely absence of deadlock and validity of an ecoin during the execution of the protocol. This paper assumes a cooperative customer and will prove that the protocol is executing according to its description.

Keywords: Model, Verification, Micropayment.

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

Authors: Rafik Massoudi

Abstract:

Irish identity continues to be discussed in various fields including social science, culture, literary humanities as well as political debates. In this context, Irishness had been usurped for a long time by the hegemonic power of the British Empire. That is why, Irish writers, in general, and Seamus Heaney along with William Butler Yeats, in particular, endeavored to retrieve this lost identity by shedding light on Irish history, folklore, communal traditions, landscape, indigenous people, language as well as culture. In this context, we may speak of a decolonizing attempt that allowed these writers to represent the autonomous Irish subjectivity by establishing an ethical relationship based on an extraordinary approach to the represented alterity. This article, indeed, places itself within the arena of postmodern, postcolonial discussions of the issue of identity and, particularly, of Irishness.

Keywords: Identity, Irishess, narration, postcolonialism.

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

Authors: Abhijit Mitra, Pranab Kumar Banerjee, C. Ardil

Abstract:

We introduce an effective approach for automatic offline au- thentication of handwritten samples where the forgeries are skillfully done, i.e., the true and forgery sample appearances are almost alike. Subtle details of temporal information used in online verification are not available offline and are also hard to recover robustly. Thus the spatial dynamic information like the pen-tip pressure characteristics are considered, emphasizing on the extraction of low density pixels. The points result from the ballistic rhythm of a genuine signature which a forgery, however skillful that may be, always lacks. Ten effective features, including these low density points and den- sity ratio, are proposed to make the distinction between a true and a forgery sample. An adaptive decision criteria is also derived for better verification judgements.

Keywords: Handwritten document verification, Skilled forgeries, Low density pixels, Adaptive decision boundary.

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

Authors: Salim Istyaq

Abstract:

As we know, number of Internet users are increasing drastically. Now, people are using different online services provided by banks, colleges/schools, hospitals, online utility, bill payment and online shopping sites. To access online services, text-based authentication system is in use. The text-based authentication scheme faces some drawbacks with usability and security issues that bring troubles to users. The core element of computational trust is identity. The aim of the paper is to make the system more compliable for the imposters and more reliable for the users, by using the graphical authentication approach. In this paper, we are using the more powerful tool of encoding the options in graphical QR format and also there will be the acknowledgment which will send to the user’s mobile for final verification. The main methodology depends upon the encryption option and final verification by confirming a set of pass phrase on the legal users, the outcome of the result is very powerful as it only gives the result at once when the process is successfully done. All processes are cross linked serially as the output of the 1st process, is the input of the 2nd and so on. The system is a combination of recognition and pure recall based technique. Presented scheme is useful for devices like PDAs, iPod, phone etc. which are more handy and convenient to use than traditional desktop computer systems.

Keywords: Graphical Password, OTP, QR Codes, Recognition based graphical user authentication, usability and security.

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

Authors: Pibool Waijittragum

Abstract:

The mosques have been appearance in Thailand since Ayutthaya Kingdom (1350 to 1767 A.D.) Until today, more than 400 years later; there are many styles of art form behind their structure. This research intended to identify Islamic Art in Thai mosques. A framework was applied using qualitative research methods; Thai Muslims with dynamic roles in Islamic culture were interviewed. In addition, a field survey of 40 selected mosques from 175 Thai mosques was studied. Data analysis will be according to the pattern of each period. The identification of Islamic Art in Thai Mosques are 1) the image of Thai identity: with Thai traditional art style and Government policy. 2) The image of the Ethnological identity: with the traditional culture of Asian Muslims in Thailand. 3) The image of the Nostalgia identity: with Islamic and Arabian conservative style. 4) The image of the Neo Classic identity: with Neo – Classic and Contemporary art. 5) The image of the new identity: with Post Modern and Deconstruction art.

Keywords: Islamic Art, Thai Mosques, Floral Arabesque, Geometric Form, Arabic Calligraphy.

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

Authors: A. Arjomand Kermani, N. Charbgoo, M. Alalhesabi

Abstract:

In the situation of great acceleration of changes and the need for new developments in the cities on one hand and conservation and regeneration approaches on the other hand, place identity and its relation with heritage context have taken on new importance. This relation is generally mutual and complex one. The significant point in this relation is that the process of identifying something as heritage rather than just historical  phenomena, brings that which may be inherited into the realm of identity. In planning and urban design as well as environmental psychology and phenomenology domain, place identity and its attributes and components were studied and discussed. However, the relation between physical environment (especially heritage) and identity has been neglected in the planning literature. This article aims to review the knowledge on this field and develop a model on the influence and relation of these two major concepts (heritage and identity). To build this conceptual model, we draw on available literature in environmental psychology as well as planning on place identity and heritage environment using a descriptive-analytical methodology to understand how they can inform the planning strategies and governance policies. A cross-disciplinary analysis is essential to understand the nature of place identity and heritage context and develop a more holistic model of their relationship in order to be employed in planning process and decision making. Moreover, this broader and more holistic perspective would enable both social scientists and planners to learn from one another’s expertise for a fuller understanding of community dynamics. The result indicates that a combination of these perspectives can provide a richer understanding—not only of how planning impacts our experience of place, but also how place identity can impact community planning and development.

Keywords: heritage, Inter-disciplinary study, Place identity, planning

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

Authors: Muñoz-Sanchez, Victor Manuel, Perez-Flores, Antonio Manuel

Abstract:

The main objective of this paper is to establish the relationship between models of state organization and the various types of collective identity expressed by the Spanish. The question of nationalism and identity ascription in Spain has always been a topic of special importance due to the presence in that country of territories where the population emits very different opinions of nationalist sentiment than the rest of Spain. The current situation of sovereignty challenge of Catalonia to the central government exemplifies the importance of the subject matter. In order to analyze this process of interrelation, we use a secondary data mining by applying the multiple correspondence analysis technique (MCA). As a main result a typology of four types of expression of collective identity based on models of State organization are shown, which are connected with the party position on this issue.

Keywords: Models of organization of the state, nationalism, collective identity, Spain, political parties.

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

Authors: Marichela Sepe

Abstract:

Massive use of places with strong tourist attraction with the consequent possibility of losing place-identity produces harmful effects on cities and their users. In order to mitigate this risk, areas close to such places can be identified so as to widen the visitor-s range of action and offer alternative activities integrated with the main site. The cultural places and appropriate activities can be identified using a method of analysis and design able to trace the identity of the places, their characteristics and potential, and to provide a sustainable improvement. The aim of this work is to propose PlaceMaker as a method of urban analysis and design which both detects elements that do not feature in traditional mapping and which constitute the contemporary identity of the places, and identifies appropriate project interventions. Two final complex maps – the first of analysis and the second of design – respectively represent the identity of places and project interventions. In order to illustrate the method-s potential; the results of the experimentation carried out in the Trevi-Pantheon route in Rome and the appropriate interventions to decongest the area are illustrated.

Keywords: Place-identity, PlaceMaker method, sustainablefruition, tourist attractions.

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

Authors: Hans Lödén

Abstract:

This article discusses superordinate national identity as a means for immigrants integration into democratic polities. It is suggested that a superordinate national identity perceived as inclusive, by immigrants and by the native population, would be conducive to such integration. Command of the dominant language of society is seen as most important of the inclusive criteria. Other such criteria are respect of the country's political institutions and feelings of belonging to the country where you live. The argument is supported by data, showing a majority in favour of inclusive criteria for 'Swedishness', from a recent study among 1000 secondary school students of 'Swedish' and non-'Swedish' backgrounds.

Keywords: Democratic state, exclusion, immigration, inclusion, superordinate national identity, Sweden.

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

Authors: Joanne Muscat

Abstract:

The study explored the question of who am I? As a (re)construction of cultural identity by delving into globalization, communication, and social change in Malta during a historical moment when Malta became a European Union Member State. Three objectives guided this qualitative study. Firstly the study reviewed European Union (EU) policies that regulate broadcasting and their implementation in Member States, whilst meeting the challenges of globalization and new media technology. Secondly the research investigated the changes of the media landscape via organizational structures, programs and television (TV) content. Finally the study explored the impact of these transformations taking place in the way Maltese live as they (re)construct their cultural identity. Despite the choices available to the Maltese audience, old local traditions and new foreign customs coexist as informants continue to (re)construct their cultural identity and define who they are.

Keywords: Cultural Identity, Globalization, Transnational Media.

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

Authors: Zuraidasahana Zulkarnain, Mohd Shafry Mohd Rahim, Nor Anita Fairos Ismail, Mohd Azhar M. Arsad

Abstract:

Handwritten signature is accepted widely as a biometric characteristic for personal authentication. The use of appropriate features plays an important role in determining accuracy of signature verification; therefore, this paper presents a feature based on the geometrical concept. To achieve the aim, triangle attributes are exploited to design a new feature since the triangle possesses orientation, angle and transformation that would improve accuracy. The proposed feature uses triangulation geometric set comprising of sides, angles and perimeter of a triangle which is derived from the center of gravity of a signature image. For classification purpose, Euclidean classifier along with Voting-based classifier is used to verify the tendency of forgery signature. This classification process is experimented using triangular geometric feature and selected global features. Based on an experiment that was validated using Grupo de Senales 960 (GPDS-960) signature database, the proposed triangular geometric feature achieves a lower Average Error Rates (AER) value with a percentage of 34% as compared to 43% of the selected global feature. As a conclusion, the proposed triangular geometric feature proves to be a more reliable feature for accurate signature verification.

Keywords: biometrics, euclidean classifier, feature extraction, offline signature verification, VOTING-based classifier

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

Authors: Meenakshi Mahajan, Arun Sharma, Navendu Sharma

Abstract:

Increasing use of cell phone as a medium of human interaction is playing a vital role in solving riddles of crime as well. A young girl went missing from her home late in the evening in the month of August, 2008 when her enraged relatives and villagers physically assaulted and chased her fiancée who often frequented her home. Two years later, her mother lodged a complaint against the relatives and the villagers alleging that after abduction her daughter was either sold or killed as she had failed to trace her. On investigation, a rusted cell phone with partial visible IMEI number, clothes, bangles, human skeleton etc. recovered from abandoned well in the month of May, 2011 were examined in the lab. All hopes pinned on identity of cell phone, for only linking evidence to fix the scene of occurrence supported by call detail record (CDR) and to dispel doubts about mode of sudden disappearance or death as DNA technology did not help in establishing identity of the deceased. The conventional scientific methods were used without success and international mobile equipment identification number of the cell phone could be generated by using statistical analysis followed by online verification. 

Keywords: Call detail record, Luhn algorithm, stereomicroscope.

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

Authors: Markus Kaiser, Johannes Buchmann

Abstract:

In this article, a formal specification and verification of the Rabin public-key scheme in a formal proof system is presented. 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. A major objective of this article is the presentation of the first computer-proved implementation of the Rabin public-key scheme in Isabelle/HOL. Moreover, we explicate a (computer-proven) formalization of correctness as well as a computer verification of security properties using a straight-forward computation model in Isabelle/HOL. The analysis uses a given database to prove formal properties of our implemented functions with computer support. The main task in designing a practical formalization of correctness as well as efficient computer proofs of 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 efficient formal proofs. Consequently, we get reliable proofs with a minimal error rate augmenting the used database, what 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 1535

Authors: Leila Batmany

Abstract:

This research studies the relationship between the feeling of distributive justice and national identity of the youth. The present analysis intends to experimentally investigate the various dimensions of the justice feeling and its effect on the national identity components. The study has taken justice into consideration from four different points of view on the basis of availability of valuable social sources such as power, wealth, knowledge and status in the political, economic, and cultural and status justice respectively. Furthermore, the national identity has been considered as the feeling of honour, attachment and commitment towards national society and its seven components i.e. history, language, culture, political system, religion, geographical territory and society. The 'field study' has been used as the method for the research with the individual as unit, taking 368 young between the age of 18 and 29 living in Tehran, chosen randomly according to Cochran formula. The individual samples have been randomly chosen among five districts in north, south, west, east, and centre of Tehran, based on the multistage cluster sampling. The data collection has been performed with the use of questionnaire and interview. The most important results are as follows: i) The feeling of economic justice is the weakest one among the youth. ii) The strongest and the weakest dimensions of the national identity are, respectively, the historical and the social dimension. iii) There is a positive and meaningful relationship between the feeling political and statues justice and then national identity, whereas no meaningful relationship exists between the economic and cultural justice and the national identity. iv) There is a positive and meaningful relationship between the feeling of justice in all dimensions and legitimacy of the political system. There is also such a relationship between the legitimacy of the political system and national identity. v) Generally, there is a positive and meaningful relationship between the feeling of distributive justice and national identity among the youth. vi) It is through the legitimacy of the political system that justice feeling can have an influence on the national identity.

Keywords: Distributive justice, national identity, legitimacy of political system, Cochran formula, multistage cluster sampling.

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

Authors: Rozita Borhan, Lam Kien Sieng

Abstract:

This paper describes I²C Slave implementation using I²C master obtained from the OpenCores website. This website provides free Verilog and VHDL Codes to users. The design implementation for the I²C slave is in Verilog Language and uses EDA tools for ASIC design known as ModelSim from Mentor Graphic. This tool is used for simulation and verification purposes. Common application for this I²C Master-Slave integration is also included. This paper also addresses the advantages and limitations of the said design.

Keywords: I²C, master, opencores, slave, verilog, verification.

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

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 polynomial ring setting. However, for many important applications in computer science such as satisfiability and automated verification of hardware and software, computations are performed in a Boolean ring. In this paper, we give an algorithm to show that Groebner bases computation is PSPACE 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 1959

Authors: Robert Setekera, Luuk Tiemeijer, Ramses van der Toorn

Abstract:

In this paper an extensive verification of the extraction method (published earlier) that consistently accounts for self-heating and Early effect to accurately extract both base and thermal resistance of bipolar junction transistors is presented. The method verification is demonstrated on advanced RF SiGe HBTs were the extracted results for the thermal resistance are compared with those from another published method that ignores the effect of Early effect on internal base-emitter voltage and the extracted results of the base resistance are compared with those determined from noise measurements. A self-consistency of our method in the extracted base resistance and thermal resistance using compact model simulation results is also carried out in order to study the level of accuracy of the method.

Keywords: Avalanche, Base resistance, Bipolar transistor, Compact modeling, Early voltage, Thermal resistance, Self-heating, parameter extraction.

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

Authors: Amanda Burrell, Tonia Gary, David Wright, Kumara Ward

Abstract:

This paper explores the concept of academic identity as it relates to the lecture, in particular, the digitized lecture delivered to a camera, in the absence of a student audience. Many academics have the performance aspect of the role thrust upon them with little or no training. For the purpose of this study, we look at the performance of the academic identity and examine tailored film presence coaching for its contributions toward academic identity, specifically in relation to feelings of self-confidence and diminishment of discomfort or stage fright. The case is articulated through the lens of scholar-practitioners, using expert facilitated participatory action research. It demonstrates in our sample of experienced academics, all reported some feelings of uncertainty about presenting lectures to camera prior to coaching. We share how power poses and reframing fear, produced improvements in the ease and competency of all participants. We share exactly how this insight could be adapted for self-coaching by any academic when called to present to a camera and consider the relationship between this and academic identity.

Keywords: Academic identity, embodied learning, digitized lecture, performance coaching.

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

Authors: R. Rafiemanzelat

Abstract:

One of the most recent fields of investigation in urban issues focuses on the walkability in urban spaces. Considering the importance of walkability apart from pedestrian transportation, increasing walkability will help to reduce the congestion and environmental impact. This subject also matters as it has a social life, experiential quality and economical sustainability value. This study focused on the effects of walkability and place identity on each other in urban public spaces, streets in particular, as a major indicator of their success. The theoretical aspects which examine for this purpose consist of two parts: The first will evaluate the essential components of place identity in the streets and the second one will discuss the concept of walkability and its development theories which have been derived from walkable spaces. Finally, research investigates place identity and walkability and their determinants in two major streets in different cities. The streets are Chaharbagh Street in Isfahan/Iran and Dereboyu Street in Lefkosa/North Cyprus. This study has a qualitative approach with the research method of walkability studies. The qualitative method is combined with the collection of data relating to walking behavior and place identity through an observational field study. The result will show a relationship between pedestrian-friendly spaces and identity by related variables which has obtained.

Keywords: Place identity, walkability, urban public space, streets, pedestrian-friendly.

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